:: deftheorem defines prime INT_2:def 4 :
for p being integer Number holds
( p is prime iff ( p > 1 & ( for n being Nat holds
( not n divides p or n = 1 or n = p ) ) ) );