theorem Th5: :: MODELC_2:5

for H being LTL-formula st H is next holds
H = 'X' (the_argument_of H)