let p be Nat; :: thesis:

A1: now :: thesis:

assume A2: not p is prime ; :: thesis:
assume not p <= 1 ; :: thesis:
then ex k being Element of NAT st
( k divides p & 1 < k & k < p ) by A2, Th12;
then consider k being Element of NAT such that
A3: ( k divides p & 1 < k ) and
A4: k * k <= p by Th8;
consider n being Element of NAT such that
A5: n divides p and
A6: n <= k and
A7: n is prime by A3, Th13;
take n = n; :: thesis:
thus n divides p by A5; :: thesis:
thus 1 < n by A7, Th12; :: thesis:
n * n <= k * k by A6, XREAL_1:66;
hence n * n <= p by A4, XXREAL_0:2; :: thesis:
thus n is prime by A7; :: thesis:

end;

now :: thesis:

assume A8: ( p <= 1 or ex n being Element of NAT st
( n divides p & 1 < n & n * n <= p ) ) ; :: thesis:

per cases by A8;

suppose p <= 1 ; :: thesis:

hence not p is prime by Th12; :: thesis:

end;

suppose ex n being Element of NAT st
( n divides p & 1 < n & n * n <= p ) ; :: thesis:

then consider n being Element of NAT such that
A9: n divides p and
A10: 1 < n and
A11: n * n <= p ;
n < p by A10, A11, Th2;
hence not p is prime by A9, A10, Th12; :: thesis:

end;

end;

end;

hence ( ( p <= 1 or ex n being Element of NAT st
( n divides p & 1 < n & n * n <= p & n is prime ) ) iff not p is prime ) by A1; :: thesis: