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