let H, F be LTL-formula; :: thesis: ( H is neg-inner-most & F is_subformula_of H implies F is neg-inner-most )
assume that
A1: H is neg-inner-most and
A2: F is_subformula_of H ; :: thesis: F is neg-inner-most
for G being LTL-formula st G is_subformula_of F & G is negative holds
the_argument_of G is atomic

proof

let G be LTL-formula; :: thesis: ( G is_subformula_of F & G is negative implies the_argument_of G is atomic )
assume G is_subformula_of F ; :: thesis: ( not G is negative or the_argument_of G is atomic )
then G is_subformula_of H by A2, MODELC_2:35;
hence ( not G is negative or the_argument_of G is atomic ) by A1, Def37; :: thesis: verum

end;

hence F is neg-inner-most by Def37; :: thesis: verum