let H be CTL-formula; :: thesis: ( H is ExistGlobal implies H . 1 = 3 )
assume H is ExistGlobal ; :: thesis: H . 1 = 3
then ex H1 being CTL-formula st H = EG H1 by Def18;
hence H . 1 = 3 by FINSEQ_1:41; :: thesis: verum