let p be Point of (TOP-REAL 2); :: thesis: ( Arg p in ].0,PI.[ iff p `2 > 0 )
Im (euc2cpx p) = p `2 by COMPLEX1:12;
hence ( Arg p in ].0,PI.[ iff p `2 > 0 ) by COMPLEX2:18; :: thesis: verum