theorem Th8: :: NAT_4:8

for p being Nat st ex n being Element of NAT st
( n divides p & 1 < n & n < p ) holds
ex n being Element of NAT st
( n divides p & 1 < n & n * n <= p )