let p be Nat; :: thesis: ( ex n being Element of NAT st
( n divides p & 1 < n & n < p ) implies ex n being Element of NAT st
( n divides p & 1 < n & n * n <= p ) )
given n being Element of NAT such that A1: n divides p and
A2: 1 < n and
A3: n < p ; :: thesis: ex n being Element of NAT st
( n divides p & 1 < n & n * n <= p )

per cases ( n * n <= p or n * n > p ) ;

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

take n ; :: thesis: ( n divides p & 1 < n & n * n <= p )
thus ( n divides p & 1 < n & n * n <= p ) by A1, A2, A4; :: thesis: verum

end;

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

consider k being Nat such that
A6: p = n * k by A1, NAT_D:def 3;
A7: k * k <= p

proof

assume k * k > p ; :: thesis: contradiction
then (k * k) * (n * n) > p * p by A5, XREAL_1:96;
hence contradiction by A6; :: thesis: verum

end;

take k ; :: thesis: ( k is Element of NAT & k divides p & 1 < k & k * k <= p )
n / n < (n * k) / n by A2, A3, A6, XREAL_1:74;
then 1 < (k * n) / n by A2, XCMPLX_1:60;
hence ( k is Element of NAT & k divides p & 1 < k & k * k <= p ) by A2, A6, A7, NAT_D:def 3, ORDINAL1:def 12, XCMPLX_1:89; :: thesis: verum

end;

end;