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

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