set F = FAdj (F_Rat,{3-Root(2)});
B: the carrier of (FAdj (F_Rat,{3-Root(2)})) c= the carrier of F_Real by EC_PF_1:def 1;

now :: thesis: not X^3-2 splits_in FAdj (F_Rat,{3-Root(2)})

assume X^3-2 splits_in FAdj (F_Rat,{3-Root(2)}) ; :: thesis: contradiction
then Roots ((FAdj (F_Rat,{3-Root(2)})),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 ((FAdj (F_Rat,{3-Root(2)})),X^3-2) by ENUMSET1:def 1;
hence contradiction by B, lemnotsplit; :: thesis: verum

end;

hence not X^3-2 splits_in FAdj (F_Rat,{3-Root(2)}) ; :: thesis: verum