let H be CTL-formula; :: thesis: ( H is negative implies ( not H is atomic & not H is conjunctive & not H is ExistNext & not H is ExistGlobal & not H is ExistUntill ) )
assume H is negative ; :: thesis: ( not H is atomic & not H is conjunctive & not H is ExistNext & not H is ExistGlobal & not H is ExistUntill )
then H . 1 = 0 by Lm3;
hence ( not H is atomic & not H is conjunctive & not H is ExistNext & not H is ExistGlobal & not H is ExistUntill ) by Lm4, Lm5, Lm6, Lm7, Lm8; :: thesis: verum