let p be Nat; :: thesis: ( ( p <= 1 or ex n being Element of NAT st
( n divides p & 1 < n & n * n <= p ) ) iff not p is prime )
thus ( p is prime or p <= 1 or ex n being Element of NAT st
( n divides p & 1 < n & n * n <= p ) ) :: thesis: ( ( p <= 1 or ex n being Element of NAT st
( n divides p & 1 < n & n * n <= p ) ) implies not p is prime )

proof

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

per cases then ( p <= 1 or ex n being Element of NAT st
( n divides p & 1 < n & n < p ) ) by Th12;

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

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

end;

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

hence ( p <= 1 or ex n being Element of NAT st
( n divides p & 1 < n & n * n <= p ) ) by Th8; :: thesis: verum

end;

end;

end;

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

per cases then ( p <= 1 or ex n being Element of NAT st
( n divides p & 1 < n & n * n <= p ) ) ;

suppose p <= 1 ; :: thesis: not p is prime

hence not p is prime by INT_2:def 4; :: thesis: verum

end;

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

then consider n being Element of NAT such that
A1: n divides p and
A2: 1 < n and
A3: n * n <= p ;
n * 1 < n * n by A2, XREAL_1:68;
hence not p is prime by A1, A3, INT_2:def 4; :: thesis: verum

end;

end;