:: deftheorem defines Label_ MODELC_3:def 42 :
for v being neg-inner-most LTL-formula
for N being strict LTLnode over v holds Label_ N = { x where x is Subset of atomic_LTL : ( atomic_LTL N c= x & Neg_atomic_LTL N misses x ) } ;