let H be LTL-formula; :: thesis: ( ( H is conjunctive or H is disjunctive or H is Until or H is Release ) & H is neg-inner-most implies ( the_left_argument_of H is neg-inner-most & the_right_argument_of H is neg-inner-most ) )
assume that
A1: ( H is conjunctive or H is disjunctive or H is Until or H is Release ) and
A2: H is neg-inner-most ; :: thesis: ( the_left_argument_of H is neg-inner-most & the_right_argument_of H is neg-inner-most )
set F2 = the_right_argument_of H;
A3: the_right_argument_of H is_subformula_of H by A1, MODELC_2:31;
A4: for G being LTL-formula st G is_subformula_of the_right_argument_of H & G is negative holds
the_argument_of G is atomic by A3, A2, MODELC_2:35;
set F1 = the_left_argument_of H;
A5: the_left_argument_of H is_subformula_of H by A1, MODELC_2:31;
for G being LTL-formula st G is_subformula_of the_left_argument_of H & G is negative holds
the_argument_of G is atomic by A5, A2, MODELC_2:35;
hence ( the_left_argument_of H is neg-inner-most & the_right_argument_of H is neg-inner-most ) by A4; :: thesis: verum