:: deftheorem defines atomic MODELC_2:def 11 :
for H being LTL-formula holds
( H is atomic iff ex n being Nat st H = atom. n );