let z be Element of COMPLEX ; :: thesis: for p being Point of (TOP-REAL 2) st ( z = euc2cpx p or p = cpx2euc z ) holds
Arg z = Arg p
let p be Point of (TOP-REAL 2); :: thesis: ( ( z = euc2cpx p or p = cpx2euc z ) implies Arg z = Arg p )
assume A1: ( z = euc2cpx p or p = cpx2euc z ) ; :: thesis: Arg z = Arg p

per cases ( z = euc2cpx p or p = cpx2euc z ) by A1;

suppose z = euc2cpx p ; :: thesis: Arg z = Arg p

hence Arg z = Arg p ; :: thesis: verum

end;

suppose p = cpx2euc z ; :: thesis: Arg z = Arg p

hence Arg z = Arg p by Th1; :: thesis: verum

end;

end;