theorem :: INT_2:31

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