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 ; :: thesis: verum