theorem :: ORDERS_5:78

for A being transitive RelStr
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