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