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