theorem Th6: :: ARROW:6

for A being non empty set
for a, b being Element of A
for o99 being Element of LinOrders A st a <=_ o99,b & b <=_ o99,a holds
a = b by Def2;