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:28;
hence ( Arg p in ].0 ,PI .[ iff p `2 > 0 ) by COMPLEX2:27; :: thesis: verum