theorem :: EUCLID_3:30

for p being Point of (TOP-REAL 2) st Arg p = 0 holds
( p = |[|.p.|,0]| & p `2 = 0 )