theorem Th27: :: NUMBER08:27

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