2 in INT by NUMBERS:17;
then reconsider p = 2 as Element of INT.Ring ;
take p ; :: thesis: p is prime
p is prime by INT_2:28;
hence p is prime ; :: thesis: verum