:: deftheorem defines euc2cpx EUCLID_3:def 2 :
for p being Point of (TOP-REAL 2) holds euc2cpx p = (p `1) + ((p `2) * <i>);