:: deftheorem defines atomic MODELC_1:def 14 :
for H being CTL-formula holds
( H is atomic iff ex n being Element of NAT st H = atom. n );