theorem Th27: :: HEYTING3:27

for k being Element of NAT holds PFBrt (1,k) <> {{}}