theorem Th39: :: NAT_3:39

pfexp 1 = EmptyBag SetPrimes