atom. n is Element of LTL_WFF by Def9;
hence atom. n is LTL-formula-like by Def10; :: thesis: verum