atom. n is Element of CTL_WFF by Def12;
hence atom. n is CTL-formula-like by Def13; :: thesis: verum