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