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 Th108, Th109;
then the_argument_of G is_proper_subformula_of G by Th117;
hence the_argument_of G is_subformula_of G by Def102; :: thesis: verum