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 A1: ( 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_right_argument_of H is_immediate_constituent_of H by MODELC_2:22, MODELC_2:23, MODELC_2:24, MODELC_2:25;
then A2: the_right_argument_of H is_proper_subformula_of H by MODELC_2:29;
the_left_argument_of H is_immediate_constituent_of H by A1, MODELC_2:22, MODELC_2:23, MODELC_2:24, MODELC_2:25;
then the_left_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 A2; :: thesis: verum