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