let G be LTL-formula; :: thesis: ( ( G is conjunctive or G is disjunctive or G is Until or G is Release ) implies ( the_left_argument_of G is_subformula_of G & the_right_argument_of G is_subformula_of G ) )
assume A1: ( G is conjunctive or G is disjunctive or G is Until or G is Release ) ; :: thesis: ( the_left_argument_of G is_subformula_of G & the_right_argument_of G is_subformula_of G )
then the_right_argument_of G is_immediate_constituent_of G by Th22, Th23, Th24, Th25;
then A2: the_right_argument_of G is_proper_subformula_of G by Th29;
the_left_argument_of G is_immediate_constituent_of G by A1, Th22, Th23, Th24, Th25;
then the_left_argument_of G is_proper_subformula_of G by Th29;
hence ( the_left_argument_of G is_subformula_of G & the_right_argument_of G is_subformula_of G ) by A2; :: thesis: verum