let a be Element of R; :: thesis: ( a is P -negative implies ( not a is zero & not a is P -positive ) )
assume a is P -negative ; :: thesis: ( not a is zero & not a is P -positive )
then A: a < P, 0. R by x2;
then a <= P, 0. R ;
then B: - (- a) in - P ;
now :: thesis: not a in P \ {(0. R)}
assume a in P \ {(0. R)} ; :: thesis: contradiction
then a is P -positive ;
then 0. R < P,a by x1;
then 0. R <= P,a ;
then a in P /\ (- P) by B;
then a in {(0. R)} by REALALG1:def 7;
hence contradiction by A, TARSKI:def 1; :: thesis: verum
end;
hence ( not a is zero & not a is P -positive ) by A; :: thesis: verum