let H be LTL-formula; :: thesis: ( ( H is negative or H is next ) implies {(the_argument_of H)} is Subset of (Subformulae H) )
assume ( H is negative or H is next ) ; :: thesis: {(the_argument_of H)} is Subset of (Subformulae H)
then the_argument_of H is_subformula_of H by Lm7;
hence {(the_argument_of H)} is Subset of (Subformulae H) by Lm9; :: thesis: verum