theorem :: ZF_LANG1:134

WFF c= bool [:NAT,NAT:]