reconsider p = 2 as Element of INT.Ring by INT_1:def 2;
p <> 0. INT.Ring ;
hence ex b₁ being Element of INT.Ring st
( b₁ is prime & not b₁ is zero ) by STRUCT_0:def 12, INT_2:28; :: thesis: verum