set X = { x where x is CTL-formula : x is atomic } ;
{ x where x is CTL-formula : x is atomic } c= CTL_WFF

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is CTL-formula : x is atomic } or y in CTL_WFF )
assume y in { x where x is CTL-formula : x is atomic } ; :: thesis: y in CTL_WFF
then ex x being CTL-formula st
( y = x & x is atomic ) ;
hence y in CTL_WFF by Th1; :: thesis: verum

end;

hence { x where x is CTL-formula : x is atomic } is Subset of CTL_WFF ; :: thesis: verum