H is Element of LTL_WFF by Def10;
then 'X' H is Element of LTL_WFF by Def9;
hence 'X' H is LTL-formula-like ; :: thesis: verum