theorem Th14: :: NAT_4:14

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