:: deftheorem Def7 defines @ NAT_LAT:def 7 :
for k being Nat st k > 0 holds
@ k = k;