let H be CTL-formula; ( 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 A1:
H is atomic
; ( not H is negative & not H is conjunctive & not H is ExistNext & not H is ExistGlobal & not H is ExistUntill )
then A2:
not H . 1 = 1
by Lm8;
A3:
not H . 1 = 3
by A1, Lm8;
A4:
not H . 1 = 2
by A1, Lm8;
A5:
not H . 1 = 4
by A1, Lm8;
not H . 1 = 0
by A1, Lm8;
hence
( not H is negative & not H is conjunctive & not H is ExistNext & not H is ExistGlobal & not H is ExistUntill )
by A2, A4, A3, A5, Lm3, Lm4, Lm5, Lm6, Lm7; verum