theorem Th25: :: ORDERS_5:16

for A being non empty RelStr
for a1, a2 being Element of A holds
( not A is strongly_connected or a1 <= a2 or a2 <= a1 )