theorem Th33: :: NAT_3:33

for n being Nat
for x being set st x in dom (pfexp n) holds
x is Prime