:: deftheorem defines `2 EUCLID:def 10 :
for p being Point of (TOP-REAL 2) holds p `2 = p . 2;