theorem Th12: :: NAT_4:12

for p being Nat holds
( ( p <= 1 or ex n being Element of NAT st
( n divides p & 1 < n & n < p ) ) iff not p is prime )