theorem :: NAT_5:22

for n being Nat holds
( n is prime iff ( (((n -' 1) !) + 1) mod n = 0 & n > 1 ) )