theorem Th27: :: ORDERS_5:18

for A being non empty RelStr
for a1, a2 being Element of A st A is connected & a1 <> a2 & not a1 <= a2 holds
a2 <= a1