let A be non empty set ; :: thesis: for a, b being Element of A
for o, o' being Element of LinOrders A holds
( not ( ( a <_ o,b implies a <_ o',b ) & ( a <_ o',b implies a <_ o,b ) & ( b <_ o,a implies b <_ o',a ) & ( b <_ o',a implies b <_ o,a ) & not ( a <_ o,b iff a <_ o',b ) ) & not ( ( a <_ o,b implies a <_ o',b ) & ( a <_ o',b implies a <_ o,b ) & not ( ( a <_ o,b implies a <_ o',b ) & ( a <_ o',b implies a <_ o,b ) & ( b <_ o,a implies b <_ o',a ) & ( b <_ o',a implies b <_ o,a ) ) ) )
let a, b be Element of A; :: thesis: for o, o' being Element of LinOrders A holds
( not ( ( a <_ o,b implies a <_ o',b ) & ( a <_ o',b implies a <_ o,b ) & ( b <_ o,a implies b <_ o',a ) & ( b <_ o',a implies b <_ o,a ) & not ( a <_ o,b iff a <_ o',b ) ) & not ( ( a <_ o,b implies a <_ o',b ) & ( a <_ o',b implies a <_ o,b ) & not ( ( a <_ o,b implies a <_ o',b ) & ( a <_ o',b implies a <_ o,b ) & ( b <_ o,a implies b <_ o',a ) & ( b <_ o',a implies b <_ o,a ) ) ) )
let o, o' be Element of LinOrders A; :: thesis: ( not ( ( a <_ o,b implies a <_ o',b ) & ( a <_ o',b implies a <_ o,b ) & ( b <_ o,a implies b <_ o',a ) & ( b <_ o',a implies b <_ o,a ) & not ( a <_ o,b iff a <_ o',b ) ) & not ( ( a <_ o,b implies a <_ o',b ) & ( a <_ o',b implies a <_ o,b ) & not ( ( a <_ o,b implies a <_ o',b ) & ( a <_ o',b implies a <_ o,b ) & ( b <_ o,a implies b <_ o',a ) & ( b <_ o',a implies b <_ o,a ) ) ) )
thus not ( ( a <_ o,b implies a <_ o',b ) & ( a <_ o',b implies a <_ o,b ) & ( b <_ o,a implies b <_ o',a ) & ( b <_ o',a implies b <_ o,a ) & not ( a <_ o,b iff a <_ o',b ) ) ; :: thesis: not ( ( a <_ o,b implies a <_ o',b ) & ( a <_ o',b implies a <_ o,b ) & not ( ( a <_ o,b implies a <_ o',b ) & ( a <_ o',b implies a <_ o,b ) & ( b <_ o,a implies b <_ o',a ) & ( b <_ o',a implies b <_ o,a ) ) )
assume A1: ( a <_ o,b iff a <_ o',b ) ; :: thesis: ( ( a <_ o,b implies a <_ o',b ) & ( a <_ o',b implies a <_ o,b ) & ( b <_ o,a implies b <_ o',a ) & ( b <_ o',a implies b <_ o,a ) )
hence ( a <_ o,b iff a <_ o',b ) ; :: thesis: ( b <_ o,a iff b <_ o',a )

hereby :: thesis: ( b <_ o',a implies b <_ o,a )

assume b <_ o,a ; :: thesis: b <_ o',a
then ( a <> b & b <=_ o,a ) by Th4;
hence b <_ o',a by A1, Th6; :: thesis: verum

end;

assume b <_ o',a ; :: thesis: b <_ o,a
then ( a <> b & b <=_ o',a ) by Th4;
hence b <_ o,a by A1, Th6; :: thesis: verum