theorem :: INT_2:31

for l being Nat st l >= 2 holds
ex p being Element of NAT st
( p is prime & p divides l )