:: deftheorem defines neg-inner-most MODELC_3:def 37 :
for H being LTL-formula holds
( H is neg-inner-most iff for G being LTL-formula st G is_subformula_of H & G is negative holds
the_argument_of G is atomic );