let F be preordered Field; :: thesis: for P being Preordering of F holds /\ (P,F) = P
let P be Preordering of F; :: thesis: /\ (P,F) = P
set M = /\ (P,F);

A: now :: thesis: for o being object st o in P holds
o in /\ (P,F)

let o be object ; :: thesis: ( o in P implies o in /\ (P,F) )
assume A1: o in P ; :: thesis: o in /\ (P,F)
then reconsider a = o as Element of F ;
for O being Ordering of F st P c= O holds
a in O by A1;
hence o in /\ (P,F) ; :: thesis: verum

end;

now :: thesis: for o being object st o in /\ (P,F) holds
o in P

let o be object ; :: thesis: ( o in /\ (P,F) implies o in P )
assume o in /\ (P,F) ; :: thesis: o in P
then consider a being Element of F such that
A: ( o = a & ( for O being Ordering of F st P c= O holds
a in O ) ) ;

now :: thesis: a in P

assume B: not a in P ; :: thesis: contradiction
then not - (- a) in P ;
then reconsider P1 = P + ((- a) * P) as Preordering of F by T2;
consider O being Ordering of F such that
H: P1 c= O by T1a;
H1: ( 0. F in P & 1. F in P ) by REALALG1:25;
then - a in P1 by P2;
then X: - (- a) in - O by H;
P c= P1 by H1, P1;
then P c= O by H;
then a in O by A;
then a in O /\ (- O) by X;
then a in {(0. F)} by REALALG1:def 7;
then a = 0. F by TARSKI:def 1;
hence contradiction by B, REALALG1:25; :: thesis: verum

end;

hence o in P by A; :: thesis: verum

end;

hence /\ (P,F) = P by A, TARSKI:2; :: thesis: verum