set R = INT.Ring ;
set t = (1. INT.Ring) + (1. INT.Ring);
reconsider x = (1. INT.Ring) + (1. INT.Ring) as Integer ;
A: (1. INT.Ring) + (1. INT.Ring) <> 0. INT.Ring by INT_3:def 3;
T: not 2 divides 1 by INT_2:13;
not (1. INT.Ring) + (1. INT.Ring) divides 1. INT.Ring by T, INT_3:def 3, lemintr;
then B: (1. INT.Ring) + (1. INT.Ring) is not Unit of INT.Ring by GCD_1:def 2;
now :: thesis: for a, b being Element of INT.Ring holds
( not (1. INT.Ring) + (1. INT.Ring) divides a * b or (1. INT.Ring) + (1. INT.Ring) divides a or (1. INT.Ring) + (1. INT.Ring) divides b )
let a, b be Element of INT.Ring; :: thesis: ( not (1. INT.Ring) + (1. INT.Ring) divides a * b or (1. INT.Ring) + (1. INT.Ring) divides a or (1. INT.Ring) + (1. INT.Ring) divides b )
assume C1: (1. INT.Ring) + (1. INT.Ring) divides a * b ; :: thesis: ( (1. INT.Ring) + (1. INT.Ring) divides a or (1. INT.Ring) + (1. INT.Ring) divides b )
reconsider y = a, z = b as Integer ;
set g = x gcd y;
C2: 2 divides y * z by C1, INT_3:def 3, lemintr;
( 2 divides y or 2 divides z ) by C2, INT_5:7, INT_2:28;
hence ( (1. INT.Ring) + (1. INT.Ring) divides a or (1. INT.Ring) + (1. INT.Ring) divides b ) by INT_3:def 3, lemintr; :: thesis: verum
end;
hence ex b1 being Element of INT.Ring st b1 is prime by A, B, defprim; :: thesis: verum