let A be non empty set ; :: thesis: for o being Element of LinOrders A
for o' being Element of LinPreorders A holds
( ( for a, b being Element of A st a <_ o,b holds
a <_ o',b ) iff for a, b being Element of A holds
( a <_ o,b iff a <_ o',b ) )
let o be Element of LinOrders A; :: thesis: for o' being Element of LinPreorders A holds
( ( for a, b being Element of A st a <_ o,b holds
a <_ o',b ) iff for a, b being Element of A holds
( a <_ o,b iff a <_ o',b ) )
let o' be Element of LinPreorders A; :: thesis: ( ( for a, b being Element of A st a <_ o,b holds
a <_ o',b ) iff for a, b being Element of A holds
( a <_ o,b iff a <_ o',b ) )

hereby :: thesis: ( ( for a, b being Element of A holds
( a <_ o,b iff a <_ o',b ) ) implies for a, b being Element of A st a <_ o,b holds
a <_ o',b )

assume A1: for a, b being Element of A st a <_ o,b holds
a <_ o',b ; :: thesis: for a, b being Element of A holds
( b₃ <_ o,b₄ iff b₃ <_ o',b₄ )
let a, b be Element of A; :: thesis: ( b₁ <_ o,b₂ iff b₁ <_ o',b₂ )

per cases ( a <_ o,b or a = b or b <_ o,a ) by Th6;

suppose A2: a <_ o,b ; :: thesis: ( b₁ <_ o,b₂ iff b₁ <_ o',b₂ )

thus ( a <_ o,b iff a <_ o',b ) by A1, A2; :: thesis: verum

end;

suppose A3: a = b ; :: thesis: ( b₁ <_ o,b₂ iff b₁ <_ o',b₂ )

thus ( a <_ o,b iff a <_ o',b ) by A3, Th3; :: thesis: verum

end;

suppose A4: b <_ o,a ; :: thesis: ( b₁ <_ o,b₂ iff b₁ <_ o',b₂ )

A5: b <_ o',a by A1, A4;
thus ( a <_ o,b iff a <_ o',b ) by A4, A5, Th4; :: thesis: verum

end;

end;

end;

thus ( ( for a, b being Element of A holds
( a <_ o,b iff a <_ o',b ) ) implies for a, b being Element of A st a <_ o,b holds
a <_ o',b ) ; :: thesis: verum