theorem :: EULER_1:20

for n being Nat st n is prime holds
Euler n = n - 1