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