let H be CTL-formula; :: thesis: ( H is atomic or H is negative or H is conjunctive or H is ExistNext or H is ExistGlobal or H is ExistUntill )
A1: H is Element of CTL_WFF by Def13;
assume A2: ( not H is atomic & not H is negative & not H is conjunctive & not H is ExistNext & not H is ExistGlobal & not H is ExistUntill ) ; :: thesis: contradiction
then atom. 0 <> H ;
then A3: not atom. 0 in {H} by TARSKI:def 1;

A4: now :: thesis: for p being FinSequence of NAT st p in CTL_WFF \ {H} holds
EG p in CTL_WFF \ {H}

let p be FinSequence of NAT ; :: thesis: ( p in CTL_WFF \ {H} implies EG p in CTL_WFF \ {H} )
assume A5: p in CTL_WFF \ {H} ; :: thesis: EG p in CTL_WFF \ {H}
then reconsider H1 = p as CTL-formula by Def13;
EG H1 <> H by A2;
then A6: not EG p in {H} by TARSKI:def 1;
EG p in CTL_WFF by A5, Def12;
hence EG p in CTL_WFF \ {H} by A6, XBOOLE_0:def 5; :: thesis: verum

end;

A7: now :: thesis: for p being FinSequence of NAT st p in CTL_WFF \ {H} holds
EX p in CTL_WFF \ {H}

let p be FinSequence of NAT ; :: thesis: ( p in CTL_WFF \ {H} implies EX p in CTL_WFF \ {H} )
assume A8: p in CTL_WFF \ {H} ; :: thesis: EX p in CTL_WFF \ {H}
then reconsider H1 = p as CTL-formula by Def13;
EX H1 <> H by A2;
then A9: not EX p in {H} by TARSKI:def 1;
EX p in CTL_WFF by A8, Def12;
hence EX p in CTL_WFF \ {H} by A9, XBOOLE_0:def 5; :: thesis: verum

end;

A10: now :: thesis: for p, q being FinSequence of NAT st p in CTL_WFF \ {H} & q in CTL_WFF \ {H} holds
p '&' q in CTL_WFF \ {H}

let p, q be FinSequence of NAT ; :: thesis: ( p in CTL_WFF \ {H} & q in CTL_WFF \ {H} implies p '&' q in CTL_WFF \ {H} )
assume that
A11: p in CTL_WFF \ {H} and
A12: q in CTL_WFF \ {H} ; :: thesis: p '&' q in CTL_WFF \ {H}
reconsider F = p, G = q as CTL-formula by A11, A12, Def13;
F '&' G <> H by A2;
then A13: not p '&' q in {H} by TARSKI:def 1;
p '&' q in CTL_WFF by A11, A12, Def12;
hence p '&' q in CTL_WFF \ {H} by A13, XBOOLE_0:def 5; :: thesis: verum

end;

A14: now :: thesis: for p being FinSequence of NAT st p in CTL_WFF \ {H} holds
'not' p in CTL_WFF \ {H}

let p be FinSequence of NAT ; :: thesis: ( p in CTL_WFF \ {H} implies 'not' p in CTL_WFF \ {H} )
assume A15: p in CTL_WFF \ {H} ; :: thesis: 'not' p in CTL_WFF \ {H}
then reconsider H1 = p as CTL-formula by Def13;
'not' H1 <> H by A2;
then A16: not 'not' p in {H} by TARSKI:def 1;
'not' p in CTL_WFF by A15, Def12;
hence 'not' p in CTL_WFF \ {H} by A16, XBOOLE_0:def 5; :: thesis: verum

end;

A17: now :: thesis: for p, q being FinSequence of NAT st p in CTL_WFF \ {H} & q in CTL_WFF \ {H} holds
p EU q in CTL_WFF \ {H}

let p, q be FinSequence of NAT ; :: thesis: ( p in CTL_WFF \ {H} & q in CTL_WFF \ {H} implies p EU q in CTL_WFF \ {H} )
assume that
A18: p in CTL_WFF \ {H} and
A19: q in CTL_WFF \ {H} ; :: thesis: p EU q in CTL_WFF \ {H}
reconsider F = p, G = q as CTL-formula by A18, A19, Def13;
F EU G <> H by A2;
then A20: not p EU q in {H} by TARSKI:def 1;
p EU q in CTL_WFF by A18, A19, Def12;
hence p EU q in CTL_WFF \ {H} by A20, XBOOLE_0:def 5; :: thesis: verum

end;

A21: now :: thesis: for n being Element of NAT holds atom. n in CTL_WFF \ {H}

let n be Element of NAT ; :: thesis: atom. n in CTL_WFF \ {H}
atom. n <> H by A2;
then A22: not atom. n in {H} by TARSKI:def 1;
atom. n in CTL_WFF by Def12;
hence atom. n in CTL_WFF \ {H} by A22, XBOOLE_0:def 5; :: thesis: verum

end;

atom. 0 in CTL_WFF by Def12;
then A23: not CTL_WFF \ {H} is empty by A3, XBOOLE_0:def 5;
for a being set st a in CTL_WFF \ {H} holds
a is FinSequence of NAT by Def12;
then CTL_WFF c= CTL_WFF \ {H} by A23, A21, A14, A10, A7, A4, A17, Def12;
then H in CTL_WFF \ {H} by A1;
then not H in {H} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum