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
( b3 <_ o,b4 iff b3 <_ o9,b4 )
let a, b be Element of A; :: thesis: ( b1 <_ o,b2 iff b1 <_ o9,b2 )
per cases ( a <_ o,b or a = b or b <_ o,a ) by Th6;
suppose a <_ o,b ; :: thesis: ( b1 <_ o,b2 iff b1 <_ o9,b2 )
hence ( a <_ o,b iff a <_ o9,b ) by A1; :: thesis: verum
end;
suppose a = b ; :: thesis: ( b1 <_ o,b2 iff b1 <_ o9,b2 )
hence ( a <_ o,b iff a <_ o9,b ) by Th3; :: thesis: verum
end;
suppose A2: b <_ o,a ; :: thesis: ( b1 <_ o,b2 iff b1 <_ o9,b2 )
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