theorem :: NUMBER08:20

for p being Prime holds Euler_factorization p = p .--> (p - 1)