set F = FAdj (F_Rat,{zeta});

now :: thesis: F_Complex is not SplittingField of X^2+X+1

assume A: F_Complex is SplittingField of X^2+X+1 ; :: thesis: contradiction
X^2+X+1 splits_in FAdj (F_Rat,{zeta}) by Xsplit, FIELD_8:def 1;
then F_Complex == FAdj (F_Rat,{zeta}) by A, FIELD_8:def 1;
then F_Complex is Subfield of FAdj (F_Rat,{zeta}) by FIELD_7:def 2;
then D: the carrier of F_Complex c= the carrier of (FAdj (F_Rat,{zeta})) by EC_PF_1:def 1;
F_Real is Subfield of F_Complex by FIELD_4:7;
then the carrier of F_Real c= the carrier of F_Complex by EC_PF_1:def 1;
hence contradiction by D, ns2; :: thesis: verum

end;

hence F_Complex is not SplittingField of X^2+X+1 ; :: thesis: verum