theorem Th94: :: ORDERS_5:82

for A being Preorder
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