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 & 1 < n & 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 A2: 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; :: thesis: verum

end;

suppose A3: 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
A4: p = n * k by A1, NAT_D:def 3;
n / n < (n * k) / n by A1, A4, XREAL_1:76;
then A5: 1 < (k * n) / n by A1, XCMPLX_1:60;
A6: k * k <= p

proof

assume k * k > p ; :: thesis: contradiction
then (k * k) * (n * n) > p * p by A3, XREAL_1:98;
hence contradiction by A4; :: thesis: verum

end;

take k ; :: thesis: ( k is Element of REAL & k is Element of NAT & k divides p & 1 < k & k * k <= p )
thus ( k is Element of REAL & k is Element of NAT & k divides p & 1 < k & k * k <= p ) by A1, A4, A5, A6, NAT_D:def 3, ORDINAL1:def 13, XCMPLX_1:90; :: thesis: verum

end;

end;