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