let H be CTL-formula; :: thesis: ( H is negative implies H . 1 = 0 )
assume H is negative ; :: thesis: H . 1 = 0
then ex H1 being CTL-formula st H = 'not' H1 by Def15;
hence H . 1 = 0 by FINSEQ_1:58; :: thesis: verum