let H be LTL-formula; :: thesis: ( H is next implies H . 1 = 3 )
assume H is next ; :: thesis: H . 1 = 3
then ex H1 being LTL-formula st H = 'X' H1 by Def15;
hence H . 1 = 3 by FINSEQ_1:58; :: thesis: verum