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