let H be LTL-formula; :: thesis: ( ( H is conjunctive or H is disjunctive or H is Until or H is Release ) implies ( the_left_argument_of H is_subformula_of H & the_right_argument_of H is_subformula_of H ) )
set G1 = the_left_argument_of H;
set G2 = the_right_argument_of H;
assume ( H is conjunctive or H is disjunctive or H is Until or H is Release ) ; :: thesis: ( the_left_argument_of H is_subformula_of H & the_right_argument_of H is_subformula_of H )
then ( the_left_argument_of H is_immediate_constituent_of H & the_right_argument_of H is_immediate_constituent_of H ) by MODELC_2:22, MODELC_2:23, MODELC_2:24, MODELC_2:25;
then ( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H ) by MODELC_2:29;
hence ( the_left_argument_of H is_subformula_of H & the_right_argument_of H is_subformula_of H ) by MODELC_2:def 23; :: thesis: verum