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 st ( for a being Element of F holds
( a in P iff a in O ) ) holds
O extends P
let E be ordered FieldExtension of F; :: thesis: for P being Ordering of F
for O being Ordering of E st ( for a being Element of F holds
( a in P iff a in O ) ) holds
O extends P
let P be Ordering of F; :: thesis: for O being Ordering of E st ( for a being Element of F holds
( a in P iff a in O ) ) holds
O extends P
let O be Ordering of E; :: thesis: ( ( for a being Element of F holds
( a in P iff a in O ) ) implies O extends P )
assume AS: for a being Element of F holds
( a in P iff a in O ) ; :: thesis: O extends P

A: now :: thesis: for a being object st a in P holds
a in O /\ the carrier of F

let a be object ; :: thesis: ( a in P implies a in O /\ the carrier of F )
assume a in P ; :: thesis: a in O /\ the carrier of F
then ( a in O & a in the carrier of F ) by AS;
hence a in O /\ the carrier of F by XBOOLE_0:def 4; :: thesis: verum

end;

now :: thesis: for a being object st a in O /\ the carrier of F holds
a in P

let a be object ; :: thesis: ( a in O /\ the carrier of F implies a in P )
assume a in O /\ the carrier of F ; :: thesis: a in P
then ( a in O & a in the carrier of F ) by XBOOLE_0:def 4;
hence a in P by AS; :: thesis: verum

end;

hence O extends P by A, TARSKI:2; :: thesis: verum