consider x being Element of WFF ;
reconsider x = x 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