set p = X^2+X+1 ;
set F = F_Rat ;
1. F_Rat <> 0. F_Rat ;
then H: deg X^2+X+1 = 2 by FIELD_9:18;
thus X^2+X+1 is monic ; :: thesis: ( X^2+X+1 is quadratic & X^2+X+1 is irreducible )
thus X^2+X+1 is quadratic ; :: thesis: X^2+X+1 is irreducible
I: Roots X^2+X+1 c= Roots (F_Complex,X^2+X+1) by FIELD_4:28;
F_Rat is Subfield of F_Real by FIELD_4:7;
then K: the carrier of F_Rat c= the carrier of F_Real by EC_PF_1:def 1;

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

assume X^2+X+1 is with_roots ; :: thesis: contradiction
then consider a being Element of F_Rat such that
A: a is_a_root_of X^2+X+1 by POLYNOM5:def 8;
a in Roots X^2+X+1 by A, POLYNOM5:def 10;

per cases then ( a = zeta or a = zeta ^2 ) by I, rootz, TARSKI:def 2;

suppose a = zeta ; :: thesis: contradiction

hence contradiction by lemlem, K; :: thesis: verum

end;

suppose a = zeta ^2 ; :: thesis: contradiction

hence contradiction by lemlem, K; :: thesis: verum

end;

end;

end;

hence X^2+X+1 is irreducible by H, thirred2; :: thesis: verum