:: deftheorem defines atom. MODELC_2:def 2 :
for n being Nat holds atom. n = <*(6 + n)*>;