let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in WFF or a in bool [:NAT ,NAT :] )
assume a in WFF ; :: thesis: a in bool [:NAT ,NAT :]
then reconsider H = a as ZF-formula by ZF_LANG:14;
( H c= [:NAT ,NAT :] & H = H ) ;
hence a in bool [:NAT ,NAT :] ; :: thesis: verum