set F = FAdj (F_Rat,{2-Root(2)});
C: ( X- 2-Root(2) = rpoly (1,2-Root(2)) & X+ 2-Root(2) = rpoly (1,(- 2-Root(2))) ) by FIELD_9:def 2, FIELD_9:def 3;
( rpoly (1,2-Root(2)) is Ppoly of F_Real & rpoly (1,(- 2-Root(2))) is Ppoly of F_Real ) by RING_5:51;
then A: (rpoly (1,2-Root(2))) *' (rpoly (1,(- 2-Root(2)))) is Ppoly of F_Real by RING_5:52;
X^2-2 = (1. F_Real) * ((rpoly (1,2-Root(2))) *' (rpoly (1,(- 2-Root(2))))) by C, POLYNOM3:def 10, 2splita;
then D: X^2-2 splits_in F_Real by A, FIELD_4:def 5;
{2-Root(2),(- 2-Root(2))} c= the carrier of (FAdj (F_Rat,{2-Root(2)}))

proof

( 2-Root(2) in {2-Root(2)} & {2-Root(2)} is Subset of (FAdj (F_Rat,{2-Root(2)})) ) by FIELD_6:35, TARSKI:def 1;
then reconsider a = 2-Root(2) as Element of (FAdj (F_Rat,{2-Root(2)})) ;
H: FAdj (F_Rat,{2-Root(2)}) is Subring of F_Real by FIELD_5:12;

now :: thesis: for o being object st o in {2-Root(2),(- 2-Root(2))} holds
o in the carrier of (FAdj (F_Rat,{2-Root(2)}))

let o be object ; :: thesis: ( o in {2-Root(2),(- 2-Root(2))} implies b₁ in the carrier of (FAdj (F_Rat,{2-Root(2)})) )
assume o in {2-Root(2),(- 2-Root(2))} ; :: thesis: b₁ in the carrier of (FAdj (F_Rat,{2-Root(2)}))

per cases then ( o = 2-Root(2) or o = - 2-Root(2) ) by TARSKI:def 2;

suppose o = 2-Root(2) ; :: thesis: b₁ in the carrier of (FAdj (F_Rat,{2-Root(2)}))

then o = a ;
hence o in the carrier of (FAdj (F_Rat,{2-Root(2)})) ; :: thesis: verum

end;

suppose o = - 2-Root(2) ; :: thesis: b₁ in the carrier of (FAdj (F_Rat,{2-Root(2)}))

then o = - a by H, FIELD_6:17;
hence o in the carrier of (FAdj (F_Rat,{2-Root(2)})) ; :: thesis: verum

end;

end;

end;

hence {2-Root(2),(- 2-Root(2))} c= the carrier of (FAdj (F_Rat,{2-Root(2)})) ; :: thesis: verum

end;

then B: X^2-2 splits_in FAdj (F_Rat,{2-Root(2)}) by D, 2splitb, FIELD_8:27;

now :: thesis: for E being FieldExtension of F_Rat st X^2-2 splits_in E & E is Subfield of FAdj (F_Rat,{2-Root(2)}) holds
E == FAdj (F_Rat,{2-Root(2)})

let E be FieldExtension of F_Rat ; :: thesis: ( X^2-2 splits_in E & E is Subfield of FAdj (F_Rat,{2-Root(2)}) implies E == FAdj (F_Rat,{2-Root(2)}) )
assume C: ( X^2-2 splits_in E & E is Subfield of FAdj (F_Rat,{2-Root(2)}) ) ; :: thesis: E == FAdj (F_Rat,{2-Root(2)})
then E: ( FAdj (F_Rat,{2-Root(2)}) is E -extending & E is Subfield of F_Real ) by EC_PF_1:5, FIELD_4:7;
F: F_Rat is Subfield of E by FIELD_4:7;
{2-Root(2)} is Subset of E

proof

G: Roots (F_Real,X^2-2) c= the carrier of E by E, D, C, FIELD_8:27;
2-Root(2) in Roots (F_Real,X^2-2) by 2splitb, TARSKI:def 2;
then 2-Root(2) in the carrier of E by G;
then {2-Root(2)} c= the carrier of E by TARSKI:def 1;
hence {2-Root(2)} is Subset of E ; :: thesis: verum

end;

then FAdj (F_Rat,{2-Root(2)}) is Subfield of E by F, E, FIELD_6:37;
hence E == FAdj (F_Rat,{2-Root(2)}) by C, FIELD_7:def 2; :: thesis: verum

end;

hence FAdj (F_Rat,{2-Root(2)}) is SplittingField of X^2-2 by B, FIELD_8:def 1; :: thesis: verum