theorem :: MODELC_3:66

for H being LTL-formula st H is next & H is neg-inner-most holds
the_argument_of H is neg-inner-most