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

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

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

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

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

hence ( a <_ o,b iff a <_ o9,b ) by A1; :: thesis: verum

end;

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

hence ( a <_ o,b iff a <_ o9,b ) by Th3; :: thesis: verum

end;

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

then b <_ o9,a by A1;
hence ( a <_ o,b iff a <_ o9,b ) by A2, Th4; :: thesis: verum

end;

end;

end;

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