let p be Point of (TOP-REAL 2); :: thesis: ( p <> 0. (TOP-REAL 2) implies ( Arg p < PI iff Arg (- p) >= PI ) )
assume p <> 0. (TOP-REAL 2) ; :: thesis: ( Arg p < PI iff Arg (- p) >= PI )
then A1: euc2cpx p <> 0c by Th2, Th16;
Arg (- p) = Arg (- (euc2cpx p)) by Th13;
hence ( Arg p < PI iff Arg (- p) >= PI ) by A1, COMPLEX2:16; :: thesis: verum