set F = FAdj (F_Rat,{2-Root(2)});

now :: thesis: F_Real is not SplittingField of X^2-2

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

end;

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