let H be CTL-formula; :: thesis: ( H is conjunctive implies H . 1 = 1 )
assume H is conjunctive ; :: thesis: H . 1 = 1
then consider F, G being CTL-formula such that
A1: H = F '&' G by Def16;
( H = (<*1*> ^ F) ^ G & (<*1*> ^ F) ^ G = <*1*> ^ (F ^ G) ) by A1, FINSEQ_1:45;
hence H . 1 = 1 by FINSEQ_1:58; :: thesis: verum