theorem Th70: :: COMPUT_1:71

for P being non empty primitive-recursively_closed Subset of (HFuncs NAT) holds {} in P