theorem :: EUCLID_3:33

for p being Point of (TOP-REAL 2) holds
( Arg p in ].0,PI.[ iff p `2 > 0 )