now :: thesis: for o being object holds not o in (P ^+) /\ (P ^-)

let o be object ; :: thesis: not o in (P ^+) /\ (P ^-)
assume o in (P ^+) /\ (P ^-) ; :: thesis: contradiction
then H: ( o in P ^+ & o in P ^- ) by XBOOLE_0:def 4;
then ( o in P & o in - P ) by XBOOLE_0:def 5;
then o in P /\ (- P) ;
then o in {(0. R)} by REALALG1:def 14;
hence contradiction by H, XBOOLE_0:def 5; :: thesis: verum

end;

hence (P ^+) /\ (P ^-) is empty ; :: thesis: verum