theorem Th93: :: ORDERS_5:81

for A being Preorder
for B being Subset of A st the InternalRel of A is_connected_in B holds
the InternalRel of (QuotientOrder A) is_connected_in (proj A) .: B