set F = FAdj (F_Rat,{3-CRoot(2),zeta});

now :: thesis: F_Complex is not SplittingField of X^3-2

assume A: F_Complex is SplittingField of X^3-2 ; :: thesis: contradiction
X^3-2 splits_in FAdj (F_Rat,{3-CRoot(2),zeta}) by 32split, FIELD_8:def 1;
then F_Complex == FAdj (F_Rat,{3-CRoot(2),zeta}) by A, FIELD_8:def 1;
then F_Complex is Subfield of FAdj (F_Rat,{3-CRoot(2),zeta}) by FIELD_7:def 2;
then the carrier of F_Complex c= the carrier of (FAdj (F_Rat,{3-CRoot(2),zeta})) by EC_PF_1:def 1;
hence contradiction by ff; :: thesis: verum

end;

hence F_Complex is not SplittingField of X^3-2 ; :: thesis: verum