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

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