I: F_Rat is FieldExtension of F_Rat by FIELD_4:6;
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^3-1 splits_in F_Rat

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

end;

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