:: deftheorem defines @ EUCLID_9:def 2 :
for n being Nat
for e being Point of (Euclid n) holds @ e = e;