a in P \/ (- P) by defppp;
then - a in - (P \/ (- P)) ;
then - a in (- P) \/ (- (- P)) by REALALG1:16;
hence - a is P -ordered ; :: thesis: verum