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