now :: thesis: not X^3-1 splits_in F_Real

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

end;

hence not X^3-1 splits_in F_Real ; :: thesis: verum