:: deftheorem defines atomic_LTL MODELC_3:def 40 :
for v being neg-inner-most LTL-formula
for N being strict LTLnode over v holds atomic_LTL N = { x where x is LTL-formula : ( x is atomic & x in the LTLold of N ) } ;