for G being LTL-formula st ( G is negative or G is next ) holds
the_argument_of G is_subformula_of G