let a be Element of R; :: thesis: ( a is P -positive implies ( not a is zero & not a is P -negative ) )
assume a is P -positive ; :: thesis: ( not a is zero & not a is P -negative )
then A: 0. R < P,a by x1;
then B: 0. R <= P,a ;

now :: thesis: not a in (- P) \ {(0. R)}

assume a in (- P) \ {(0. R)} ; :: thesis: contradiction
then a is P -negative ;
then - (0. R) < P, - a by x2, c10;
then 0. R <= P, - a ;
then - (- a) in - P ;
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 -negative ) by A; :: thesis: verum