:: deftheorem defines Arg EUCLID_3:def 3 :
for p being Point of (TOP-REAL 2) holds Arg p = Arg (euc2cpx p);