:: deftheorem defines atom. MODELC_1:def 6 :
for n being Element of NAT holds atom. n = <*(5 + n)*>;