ZF-axioms c= WFF by Def4;
hence ZF-axioms is Subset of WFF ; :: thesis: verum