let A be transitive connected RelStr ; :: thesis: for B being finite Subset of A ex s being FinSequence of A st s is B -desc_ordering
let B be finite Subset of A; :: thesis: ex s being FinSequence of A st s is B -desc_ordering
consider s being FinSequence of A such that
A1: s is B -asc_ordering by Th91;
take Rev s ; :: thesis: Rev s is B -desc_ordering
thus Rev s is B -desc_ordering by A1, Th75; :: thesis: verum