let a be Element of R; :: thesis: ( a is P -negative implies a is P -ordered )
assume a is P -negative ; :: thesis: a is P -ordered
then a in - P by XBOOLE_0:def 5;
hence a in P \/ (- P) by XBOOLE_0:def 3; :: according to REALALG2:def 7 :: thesis: verum