let A be transitive connected RelStr ; :: thesis: for B being finite Subset of A ex s being FinSequence of A st s is B -asc_ordering

let B be finite Subset of A; :: thesis: ex s being FinSequence of A st s is B -asc_ordering

the InternalRel of A is_connected_in the carrier of A by Def1;

hence ex s being FinSequence of A st s is B -asc_ordering by Th16, Th89; :: thesis: verum

let B be finite Subset of A; :: thesis: ex s being FinSequence of A st s is B -asc_ordering

the InternalRel of A is_connected_in the carrier of A by Def1;

hence ex s being FinSequence of A st s is B -asc_ordering by Th16, Th89; :: thesis: verum