theorem :: ARROW:12

for A being non empty set
for a, b being Element of A
for o, o9 being Element of LinOrders A holds
( not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) & not ( a <_ o,b iff a <_ o9,b ) ) & not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) ) ) )