let F be ordered Field; :: thesis: for E being ordered FieldExtension of F
for P being Ordering of F
for O being Ordering of E holds
( O extends P iff P c= O )
let E be ordered FieldExtension of F; :: thesis: for P being Ordering of F
for O being Ordering of E holds
( O extends P iff P c= O )
let P be Ordering of F; :: thesis: for O being Ordering of E holds
( O extends P iff P c= O )
let O be Ordering of E; :: thesis: ( O extends P iff P c= O )
H1: P \/ (- P) = the carrier of F by REALALG1:def 8;
H2: O /\ (- O) = {(0. E)} by REALALG1:def 7;
I1: ( F is Subfield of E & F is Subring of E ) by FIELD_4:def 1, FIELD_4:7;
then I2: ( the carrier of F c= the carrier of E & 0. F = 0. E ) by EC_PF_1:def 1;

now :: thesis: ( P c= O implies for a being Element of F holds
( a in P iff a in O ) )

assume AS: P c= O ; :: thesis: for a being Element of F holds
( a in P iff a in O )

now :: thesis: for a being Element of F st a in O holds
a in P

let a be Element of F; :: thesis: ( a in O implies a in P )
reconsider b = a as Element of E by I2;
I3: - b = - a by I1, FIELD_6:17;
assume B0: a in O ; :: thesis: a in P

now :: thesis: a in P

assume B1: not a in P ; :: thesis: contradiction
then a in - P by H1, XBOOLE_0:def 3;
then - a in - (- P) ;
then - (- b) in - O by AS, I3;
then b in O /\ (- O) by B0;
then b = 0. F by I2, H2, TARSKI:def 1;
hence contradiction by B1, REALALG1:25; :: thesis: verum

end;

hence a in P ; :: thesis: verum

end;

hence for a being Element of F holds
( a in P iff a in O ) by AS; :: thesis: verum

end;

hence ( O extends P iff P c= O ) by XBOOLE_0:def 4, l12; :: thesis: verum