let R be preordered Field; :: thesis: for P being Preordering of R holds
( P is maximal iff P is positive_cone )
let P be Preordering of R; :: thesis: ( P is maximal iff P is positive_cone )

hereby :: thesis: ( P is positive_cone implies P is maximal )

assume AS: P is maximal ; :: thesis: P is positive_cone

now :: thesis: for x being object st x in the carrier of R holds
x in P \/ (- P)

let x be object ; :: thesis: ( x in the carrier of R implies x in P \/ (- P) )
assume x in the carrier of R ; :: thesis: x in P \/ (- P)
then reconsider a = x as Element of R ;

now :: thesis: ( not a in P implies a in - P )

assume AS1: not a in P ; :: thesis: a in - P

now :: thesis: - a in P

assume not - a in P ; :: thesis: contradiction
then reconsider Q = P + (a * P) as Preordering of R by T2;
C: 0. R in P by REALALG1:25;
then X: P = Q by AS, P1;
1. R in P by REALALG1:25;
hence contradiction by P2, C, X, AS1; :: thesis: verum

end;

then - (- a) in - P ;
hence a in - P ; :: thesis: verum

end;

hence x in P \/ (- P) by XBOOLE_0:def 3; :: thesis: verum

end;

then the carrier of R c= P \/ (- P) ;
then P \/ (- P) = the carrier of R ;
then P is spanning ;
hence P is positive_cone ; :: thesis: verum

end;

assume AS: P is positive_cone ; :: thesis: P is maximal
assume not P is maximal ; :: thesis: contradiction
then consider Q being Preordering of R such that
A: ( P c= Q & P <> Q ) ;
P c< Q by A;
then consider a being object such that
B: ( a in Q & not a in P ) by XBOOLE_0:6;
reconsider a = a as Element of R by B;
a in - P by AS, B, XBOOLE_0:def 3;
then - a in - (- P) ;
then - (- a) in - Q by A;
then a in Q /\ (- Q) by B;
then a in {(0. R)} by REALALG1:def 7;
then a = 0. R by TARSKI:def 1;
hence contradiction by B, REALALG1:25; :: thesis: verum