H0: F_Real is Subfield of F_Complex by FIELD_4:7;
H1: Roots (F_Real,X^3-2) = { a where a is Element of F_Real : a is_a_root_of X^3-2 , F_Real } 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;

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

let o be object ; :: thesis: ( o in {3-Root(2)} implies o in Roots (F_Real,X^3-2) )
assume o in {3-Root(2)} ; :: thesis: o in Roots (F_Real,X^3-2)
then A1: o = 3-Root(2) by TARSKI:def 1;
3-Root(2) is_a_root_of X^3-2 , F_Real by LL2, FIELD_4:def 2;
hence o in Roots (F_Real,X^3-2) by A1, H1; :: thesis: verum

end;

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

let o be object ; :: thesis: ( o in Roots (F_Real,X^3-2) implies o in {3-Root(2)} )
assume o in Roots (F_Real,X^3-2) ; :: thesis: o in {3-Root(2)}
then consider a being Element of F_Real such that
B1: ( o = a & a is_a_root_of X^3-2 , F_Real ) by H1;
the carrier of F_Real c= the carrier of F_Complex by H0, EC_PF_1:def 1;
then reconsider z = a as Element of F_Complex ;
0. F_Real = 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 lemnotsplit; :: thesis: verum

end;

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

hence contradiction by lemnotsplit; :: thesis: verum

end;

end;

end;

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

end;

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