theorem Th13: :: NAT_4:13

for n, k being Nat st n divides k & 1 < n holds
ex p being Element of NAT st
( p divides k & p <= n & p is prime )