let H be LTL-formula; :: thesis: ( H is next implies H = 'X' (the_argument_of H) )
assume A1: H is next ; :: thesis: H = 'X' (the_argument_of H)
then not H is negative by Lm19;
hence H = 'X' (the_argument_of H) by A1, Def18; :: thesis: verum