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

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