Reachability from the unique source of a ranked relation

theorem MagnitudeConjecture.RankedReachability.source_reaches {V : Type u} (rank : V → ℕ) (E : V → V → Prop) (hE : ∀ (x y : V), E x y → rank x < rank y) (source : V) (hsource : ∀ (x : V), (¬∃ (y : V), E y x) → x = source) (x : V) : Relation.ReflTransGen E source x

In a relation with strictly increasing natural rank, every vertex is reachable from its unique source.