let H be CTL-formula; :: thesis: ( H is ExistNext implies H . 1 = 2 )
assume H is ExistNext ; :: thesis: H . 1 = 2
then ex H1 being CTL-formula st H = EX H1 by Def17;
hence H . 1 = 2 by FINSEQ_1:41; :: thesis: verum