ZF-axioms c= WFF

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in ZF-axioms or e in WFF )
thus ( not e in ZF-axioms or e in WFF ) by Def4; :: thesis: verum

end;

hence ZF-axioms is Subset of WFF ; :: thesis: verum