H is Element of WFF by Def9;
then 'not' H is Element of WFF by Def8;
hence 'not' H is ZF-formula-like ; :: thesis: verum