set K = FAdj (F_Rat,{3-CRoot(2)});
FAdj (F_Rat,{3-CRoot(2)}) = FAdj (F_Rat,{3-Root(2)}) by mmk;
then K: the carrier of (FAdj (F_Rat,{3-CRoot(2)})) c= the carrier of F_Real by EC_PF_1:def 1;
the carrier of (Polynom-Ring F_Rat) c= the carrier of (Polynom-Ring (FAdj (F_Rat,{3-CRoot(2)}))) by FIELD_4:10;
then reconsider p = X^2+X+1 as Element of the carrier of (Polynom-Ring (FAdj (F_Rat,{3-CRoot(2)}))) ;
M: deg p = 2 by LL, FIELD_4:20;
then reconsider p = p as non constant Element of the carrier of (Polynom-Ring (FAdj (F_Rat,{3-CRoot(2)}))) by RING_4:def 4;
L: F_Rat is Subfield of FAdj (F_Rat,{3-CRoot(2)}) by FIELD_4:7;
LC p = LC X^2+X+1 by FIELD_8:5
.= 1. F_Rat by RATFUNC1:def 7
.= 1. (FAdj (F_Rat,{3-CRoot(2)})) by L, EC_PF_1:def 1 ;
then A: p is monic by RATFUNC1:def 7;

B: now :: thesis: not p is reducible

assume p is reducible ; :: thesis: contradiction
then p is with_roots by M, thirred2;
then consider a being Element of (FAdj (F_Rat,{3-CRoot(2)})) such that
C: a is_a_root_of p by POLYNOM5:def 8;
Y: Roots p c= Roots (F_Complex,p) by FIELD_4:28;
Z: Roots (F_Complex,p) = {zeta,(zeta ^2)} by rootz, mmo;
a in Roots p by C, POLYNOM5:def 10;

per cases then ( a = zeta or a = zeta ^2 ) by Z, Y, 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;

H: Roots (F_Complex,X^2+X+1) = { a where a is Element of F_Complex : a is_a_root_of X^2+X+1 , F_Complex } by FIELD_4:def 4;
zeta in Roots (F_Complex,X^2+X+1) by rootz, TARSKI:def 2;
then consider a being Element of F_Complex such that
I: ( a = zeta & a is_a_root_of X^2+X+1 , F_Complex ) by H;
0. F_Complex = Ext_eval (X^2+X+1,zeta) by I, FIELD_4:def 2
.= Ext_eval (p,zeta) by FIELD_8:6 ;
hence MinPoly (zeta,(FAdj (F_Rat,{3-CRoot(2)}))) = X^2+X+1 by A, B, FIELD_6:52; :: thesis: verum