let A be non empty set ; 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; 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; ( ( 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 ( ( 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
;
for a, b being Element of A holds
( b3 <_ o,b4 iff b3 <_ o9,b4 )let a,
b be
Element of
A;
( 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
;
( b1 <_ o,b2 iff b1 <_ o9,b2 )hence
(
a <_ o,
b iff
a <_ o9,
b )
by A1;
verum end; suppose
a = b
;
( b1 <_ o,b2 iff b1 <_ o9,b2 )hence
(
a <_ o,
b iff
a <_ o9,
b )
by Th3;
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 )
; verum