set x = the Element of WFF ;
reconsider x = the Element of WFF as FinSequence of NAT by Def8;
take x ; :: thesis: x is ZF-formula-like
thus x is Element of WFF ; :: according to ZF_LANG:def 9 :: thesis: verum