let A be Preorder; :: thesis: for B being Subset of A

for s1 being FinSequence of A st s1 is B -asc_ordering holds

ex s2 being FinSequence of (QuotientOrder A) st s2 is (proj A) .: B -asc_ordering

let B be Subset of A; :: thesis: for s1 being FinSequence of A st s1 is B -asc_ordering holds

ex s2 being FinSequence of (QuotientOrder A) st s2 is (proj A) .: B -asc_ordering

let s1 be FinSequence of the carrier of A; :: thesis: ( s1 is B -asc_ordering implies ex s2 being FinSequence of (QuotientOrder A) st s2 is (proj A) .: B -asc_ordering )

assume A1: s1 is B -asc_ordering ; :: thesis: ex s2 being FinSequence of (QuotientOrder A) st s2 is (proj A) .: B -asc_ordering

then A2: the InternalRel of A is_connected_in B by Th83;

reconsider B = B as finite Subset of A by A1;

(proj A) .: B is finite ;

hence ex s2 being FinSequence of (QuotientOrder A) st s2 is (proj A) .: B -asc_ordering by A2, Th93, Th89; :: thesis: verum

for s1 being FinSequence of A st s1 is B -asc_ordering holds

ex s2 being FinSequence of (QuotientOrder A) st s2 is (proj A) .: B -asc_ordering

let B be Subset of A; :: thesis: for s1 being FinSequence of A st s1 is B -asc_ordering holds

ex s2 being FinSequence of (QuotientOrder A) st s2 is (proj A) .: B -asc_ordering

let s1 be FinSequence of the carrier of A; :: thesis: ( s1 is B -asc_ordering implies ex s2 being FinSequence of (QuotientOrder A) st s2 is (proj A) .: B -asc_ordering )

assume A1: s1 is B -asc_ordering ; :: thesis: ex s2 being FinSequence of (QuotientOrder A) st s2 is (proj A) .: B -asc_ordering

then A2: the InternalRel of A is_connected_in B by Th83;

reconsider B = B as finite Subset of A by A1;

(proj A) .: B is finite ;

hence ex s2 being FinSequence of (QuotientOrder A) st s2 is (proj A) .: B -asc_ordering by A2, Th93, Th89; :: thesis: verum