theorem Th29: :: NUMBER08:29

for n being non zero Nat
for p being object st p in dom (Euler_factorization_2 n) holds
p is Prime