:: deftheorem defines 1.REAL EUCLID:def 12 :
for n being Nat holds 1.REAL n = 1* n;