theorem Th20: :: NUMBER15:20

for n being Nat st n > 1 holds
ex p being Prime st
( p divides n & ( for q being Prime st q divides n holds
q <= p ) )