atom. n is LTL-formula-like

proof

thus atom. n is Element of LTL_WFF by Def12; :: according to MODELC_2:def 10 :: thesis: verum

end;

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