now :: thesis: not X^2+X+1 splits_in F_Real

assume X^2+X+1 splits_in F_Real ; :: thesis: contradiction
then A: {zeta,(zeta ^2)} c= the carrier of F_Real by rootz, LLsplit, FIELD_8:27;
zeta in {zeta,(zeta ^2)} by TARSKI:def 2;
hence contradiction by A, FIELD_7:def 5; :: thesis: verum

end;

hence not X^2+X+1 splits_in F_Real ; :: thesis: verum