let A be transitive RelStr ; :: thesis: for B being finite Subset of A st the InternalRel of A is_connected_in B holds

ex s being FinSequence of A st s is B -desc_ordering

let B be finite Subset of A; :: thesis: ( the InternalRel of A is_connected_in B implies ex s being FinSequence of A st s is B -desc_ordering )

assume the InternalRel of A is_connected_in B ; :: thesis: ex s being FinSequence of A st s is B -desc_ordering

then consider s being FinSequence of A such that

A1: s is B -asc_ordering by Th89;

take Rev s ; :: thesis: Rev s is B -desc_ordering

thus Rev s is B -desc_ordering by A1, Th75; :: thesis: verum

ex s being FinSequence of A st s is B -desc_ordering

let B be finite Subset of A; :: thesis: ( the InternalRel of A is_connected_in B implies ex s being FinSequence of A st s is B -desc_ordering )

assume the InternalRel of A is_connected_in B ; :: thesis: ex s being FinSequence of A st s is B -desc_ordering

then consider s being FinSequence of A such that

A1: s is B -asc_ordering by Th89;

take Rev s ; :: thesis: Rev s is B -desc_ordering

thus Rev s is B -desc_ordering by A1, Th75; :: thesis: verum