let G be LTL-formula; :: thesis: ( ( G is negative or G is next ) implies the_argument_of G is_subformula_of G )
assume ( G is negative or G is next ) ; :: thesis: the_argument_of G is_subformula_of G
then the_argument_of G is_immediate_constituent_of G by Th20, Th21;
then the_argument_of G is_proper_subformula_of G by Th29;
hence the_argument_of G is_subformula_of G ; :: thesis: verum