H is Element of WFF by Def9;
then All x,H is Element of WFF by Def8;
hence All x,H is ZF-formula-like by Def9; :: thesis: verum