let A be Preorder; :: thesis: for B being Subset of A
for s1 being FinSequence of A st s1 is B -desc_ordering holds
ex s2 being FinSequence of (QuotientOrder A) st s2 is (proj A) .: B -desc_ordering
let B be Subset of A; :: thesis: for s1 being FinSequence of A st s1 is B -desc_ordering holds
ex s2 being FinSequence of (QuotientOrder A) st s2 is (proj A) .: B -desc_ordering
let s1 be FinSequence of the carrier of A; :: thesis: ( s1 is B -desc_ordering implies ex s2 being FinSequence of (QuotientOrder A) st s2 is (proj A) .: B -desc_ordering )
assume s1 is B -desc_ordering ; :: thesis: ex s2 being FinSequence of (QuotientOrder A) st s2 is (proj A) .: B -desc_ordering
then Rev (Rev s1) is B -desc_ordering ;
then Rev s1 is B -asc_ordering by Th75;
then consider s2 being FinSequence of (QuotientOrder A) such that
A1: s2 is (proj A) .: B -asc_ordering by Th94;
take Rev s2 ; :: thesis: Rev s2 is (proj A) .: B -desc_ordering
thus Rev s2 is (proj A) .: B -desc_ordering by A1, Th75; :: thesis: verum