let H be LTL-formula; :: thesis: ( ( H is disjunctive or H is conjunctive or H is Until or H is Release ) implies ( {(the_left_argument_of H)} is Subset of (Subformulae H) & {(the_right_argument_of H)} is Subset of (Subformulae H) ) )
assume ( H is disjunctive or H is conjunctive or H is Until or H is Release ) ; :: thesis: ( {(the_left_argument_of H)} is Subset of (Subformulae H) & {(the_right_argument_of H)} is Subset of (Subformulae H) )
then ( the_left_argument_of H is_subformula_of H & the_right_argument_of H is_subformula_of H ) by Lm8;
hence ( {(the_left_argument_of H)} is Subset of (Subformulae H) & {(the_right_argument_of H)} is Subset of (Subformulae H) ) by Lm9; :: thesis: verum