atom. n is CTL-formula-like

proof

thus atom. n is Element of CTL_WFF by Def12; :: according to MODELC_1:def 13 :: thesis: verum

end;

hence atom. n is CTL-formula-like ; :: thesis: verum