:: deftheorem Def9 defines ZF-formula-like ZF_LANG:def 9 :
for IT being FinSequence of NAT holds
( IT is ZF-formula-like iff IT is Element of WFF );