theorem Th7: :: NAT_4:7

for n, p being Nat st p > 0 & n divides p & n <> 1 & n <> p holds
( 1 < n & n < p )