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

assume X^3-2 splits_in F_Real ; :: thesis: contradiction
then Roots (F_Real,X^3-2) = {3-Root(2),(3-Root(2) * zeta),(3-Root(2) * (zeta ^2))} by LLsplit, FIELD_8:29, lemroots;
then 3-Root(2) * zeta in Roots (F_Real,X^3-2) by ENUMSET1:def 1;
hence contradiction by lemnotsplit; :: thesis: verum

end;

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