:: deftheorem defines 1* EUCLID:def 11 :
for n being Nat holds 1* n = n |-> 1;