set F = FAdj (F_Rat,{3-Root(2)});
H0: ( FAdj (F_Rat,{3-Root(2)}) is Subfield of F_Complex & the carrier of (FAdj (F_Rat,{3-Root(2)})) c= the carrier of F_Real ) by FIELD_4:7, EC_PF_1:def 1;
H1: Roots ((FAdj (F_Rat,{3-Root(2)})),X^3-2) = { a where a is Element of (FAdj (F_Rat,{3-Root(2)})) : a is_a_root_of X^3-2 , FAdj (F_Rat,{3-Root(2)}) } by FIELD_4:def 4;
H2: Roots (F_Complex,X^3-2) = { a where a is Element of F_Complex : a is_a_root_of X^3-2 , F_Complex } by FIELD_4:def 4;
H3: {3-Root(2)} is Subset of the carrier of (FAdj (F_Rat,{3-Root(2)})) by FIELD_6:35;
3-Root(2) in {3-Root(2)} by TARSKI:def 1;
then reconsider z = 3-Root(2) as Element of (FAdj (F_Rat,{3-Root(2)})) by H3;

A: now :: thesis: for o being object st o in {3-Root(2)} holds
o in Roots ((FAdj (F_Rat,{3-Root(2)})),X^3-2)

let o be object ; :: thesis: ( o in {3-Root(2)} implies o in Roots ((FAdj (F_Rat,{3-Root(2)})),X^3-2) )
assume o in {3-Root(2)} ; :: thesis: o in Roots ((FAdj (F_Rat,{3-Root(2)})),X^3-2)
then A1: o = 3-Root(2) by TARSKI:def 1;
Ext_eval (X^3-2,z) = Ext_eval (X^3-2,3-Root(2)) by FIELD_7:14
.= 0. (FAdj (F_Rat,{3-Root(2)})) by LL2, FIELD_6:def 6 ;
then z is_a_root_of X^3-2 , FAdj (F_Rat,{3-Root(2)}) by FIELD_4:def 2;
hence o in Roots ((FAdj (F_Rat,{3-Root(2)})),X^3-2) by A1, H1; :: thesis: verum

end;

now :: thesis: for o being object st o in Roots ((FAdj (F_Rat,{3-Root(2)})),X^3-2) holds
o in {3-Root(2)}

let o be object ; :: thesis: ( o in Roots ((FAdj (F_Rat,{3-Root(2)})),X^3-2) implies o in {3-Root(2)} )
assume o in Roots ((FAdj (F_Rat,{3-Root(2)})),X^3-2) ; :: thesis: o in {3-Root(2)}
then consider a being Element of (FAdj (F_Rat,{3-Root(2)})) such that
B1: ( o = a & a is_a_root_of X^3-2 , FAdj (F_Rat,{3-Root(2)}) ) by H1;
the carrier of (FAdj (F_Rat,{3-Root(2)})) c= the carrier of F_Complex by H0, EC_PF_1:def 1;
then reconsider z = a as Element of F_Complex ;
0. (FAdj (F_Rat,{3-Root(2)})) = Ext_eval (X^3-2,a) by B1, FIELD_4:def 2
.= Ext_eval (X^3-2,z) by FIELD_6:11 ;
then 0. F_Complex = Ext_eval (X^3-2,z) by H0, EC_PF_1:def 1;
then z is_a_root_of X^3-2 , F_Complex by FIELD_4:def 2;
then B2: z in Roots (F_Complex,X^3-2) by H2;

now :: thesis: not z <> 3-Root(2)

assume z <> 3-Root(2) ; :: thesis: contradiction

per cases then ( z = 3-Root(2) * zeta or z = 3-Root(2) * (zeta ^2) ) by B2, lemroots, ENUMSET1:def 1;

suppose z = 3-Root(2) * zeta ; :: thesis: contradiction

hence contradiction by H0, lemnotsplit; :: thesis: verum

end;

suppose z = 3-Root(2) * (zeta ^2) ; :: thesis: contradiction

hence contradiction by H0, lemnotsplit; :: thesis: verum

end;

end;

end;

hence o in {3-Root(2)} by B1, TARSKI:def 1; :: thesis: verum

end;

hence Roots ((FAdj (F_Rat,{3-Root(2)})),X^3-2) = {3-Root(2)} by A, TARSKI:2; :: thesis: verum