theorem Th26: :: ORDERS_5:17

for A being non empty RelStr
for B being Subset of A
for a1, a2 being Element of A st the InternalRel of A is_connected_in B & a1 in B & a2 in B & a1 <> a2 & not a1 <= a2 holds
a2 <= a1