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_left_argument_of G is_immediate_constituent_of G by Th110, Th111, Th112, Th113;
then A2: the_left_argument_of G is_proper_subformula_of G by Th117;
the_right_argument_of G is_immediate_constituent_of G by A1, Th110, Th111, Th112, Th113;
then the_right_argument_of G is_proper_subformula_of G by Th117;
hence ( the_left_argument_of G is_subformula_of G & the_right_argument_of G is_subformula_of G ) by Def102, A2; :: thesis: verum