theorem :: MODELC_2:30

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