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),(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),(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),(the_right_argument_of H)} is Subset of (Subformulae H) by Lm10; :: thesis: verum