:: deftheorem defines atomic_WFF MODELC_1:def 25 :
atomic_WFF = { x where x is CTL-formula : x is atomic } ;