now :: thesis: not X^2+X+1 is reducible

assume X^2+X+1 is reducible ; :: thesis: contradiction
then consider q being Element of the carrier of (Polynom-Ring (Z/ 2)) such that
C2: ( q divides X^2+X+1 & 1 <= deg q & deg q < deg X^2+X+1 ) by RING_4:41;
deg X^2+X+1 = 2 by qua4;
then (deg q) + 1 <= 2 by C2, INT_1:7;
then ((deg q) + 1) - 1 <= 2 - 1 by XREAL_1:9;
then consider x, a being Element of (Z/ 2) such that
C3: ( x <> 0. (Z/ 2) & q = x * (rpoly (1,a)) ) by C2, XXREAL_0:1, HURWITZ:28;
consider p being Polynomial of (Z/ 2) such that
C4: X^2+X+1 = q *' p by C2, RING_4:1;
thus contradiction by C3, C4, z24; :: thesis: verum

end;

hence X^2+X+1 is irreducible ; :: thesis: verum