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