let a be object ; :: 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:4;
H c= [:NAT,NAT:] ;
hence a in bool [:NAT,NAT:] ; :: thesis: verum