let a be set ; :: thesis: ( a is ZF-formula iff a in WFF )
thus ( a is ZF-formula implies a in WFF ) :: thesis: ( a in WFF implies a is ZF-formula )

proof

assume a is ZF-formula ; :: thesis: a in WFF
then a is Element of WFF by Def9;
hence a in WFF ; :: thesis: verum

end;

assume a in WFF ; :: thesis: a is ZF-formula
hence a is ZF-formula by Def8, Def9; :: thesis: verum