:: deftheorem defines atomic_LTL MODELC_2:def 26 :
atomic_LTL = { x where x is LTL-formula : x is atomic } ;