let H be LTL-formula; :: thesis: ( H is next & H is neg-inner-most implies the_argument_of H is neg-inner-most )
assume that
A1: H is next and
A2: H is neg-inner-most ; :: thesis: the_argument_of H is neg-inner-most
set F = the_argument_of H;
A3: the_argument_of H is_subformula_of H by A1, MODELC_2:30;
for G being LTL-formula st G is_subformula_of the_argument_of H & G is negative holds
the_argument_of G is atomic by A3, A2, MODELC_2:35;
hence the_argument_of H is neg-inner-most ; :: thesis: verum