set F = FAdj (F_Rat,{3-CRoot(2),zeta});
Roots (F_Complex,X^3-2) c= the carrier of (FAdj (F_Rat,{3-CRoot(2),zeta}))

proof

A1: {3-CRoot(2),zeta} is Subset of (FAdj (F_Rat,{3-CRoot(2),zeta})) by FIELD_6:35;
( 3-Root(2) in {3-CRoot(2),zeta} & zeta in {3-CRoot(2),zeta} ) by TARSKI:def 2;
then reconsider a = 3-Root(2) , b = zeta as Element of (FAdj (F_Rat,{3-CRoot(2),zeta})) by A1;
A3: FAdj (F_Rat,{3-CRoot(2),zeta}) is Subring of F_Complex by FIELD_4:def 1;
A5: zeta * zeta = b * b by A3, FIELD_6:16;

now :: thesis: for o being object st o in Roots (F_Complex,X^3-2) holds
o in the carrier of (FAdj (F_Rat,{3-CRoot(2),zeta}))

let o be object ; :: thesis: ( o in Roots (F_Complex,X^3-2) implies b₁ in the carrier of (FAdj (F_Rat,{3-CRoot(2),zeta})) )
assume o in Roots (F_Complex,X^3-2) ; :: thesis: b₁ in the carrier of (FAdj (F_Rat,{3-CRoot(2),zeta}))

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

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

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

end;

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

then o = 3-CRoot(2) * zeta
.= a * b by A3, FIELD_6:16 ;
hence o in the carrier of (FAdj (F_Rat,{3-CRoot(2),zeta})) ; :: thesis: verum

end;

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

then o = 3-CRoot(2) * (zeta * zeta) by O_RING_1:def 1
.= a * (b * b) by A3, A5, FIELD_6:16 ;
hence o in the carrier of (FAdj (F_Rat,{3-CRoot(2),zeta})) ; :: thesis: verum

end;

end;

end;

hence Roots (F_Complex,X^3-2) c= the carrier of (FAdj (F_Rat,{3-CRoot(2),zeta})) ; :: thesis: verum

end;

then B: X^3-2 splits_in FAdj (F_Rat,{3-CRoot(2),zeta}) by LLsplit, FIELD_8:27;

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

let E be FieldExtension of F_Rat ; :: thesis: ( X^3-2 splits_in E & E is Subfield of FAdj (F_Rat,{3-CRoot(2),zeta}) implies E == FAdj (F_Rat,{3-CRoot(2),zeta}) )
assume C: ( X^3-2 splits_in E & E is Subfield of FAdj (F_Rat,{3-CRoot(2),zeta}) ) ; :: thesis: E == FAdj (F_Rat,{3-CRoot(2),zeta})
then E: E is Subfield of F_Complex by EC_PF_1:5;
then F: E is Subring of F_Complex by FIELD_5:12;
D: F_Rat is Subfield of E by FIELD_4:7;
{3-CRoot(2),zeta} is Subset of E

proof

F_Complex is E -extending by E, FIELD_4:7;
then A1: Roots (F_Complex,X^3-2) c= the carrier of E by LLsplit, C, FIELD_8:27;
( 3-Root(2) in Roots (F_Complex,X^3-2) & 3-CRoot(2) * zeta in Roots (F_Complex,X^3-2) ) by lemroots, ENUMSET1:def 1;
then reconsider a = 3-Root(2) , b = 3-CRoot(2) * zeta as Element of E by A1;
A3: not 3-CRoot(2) is zero ;
a " = 3-CRoot(2) " by E, FIELD_6:18;
then A4: (a ") * b = (3-CRoot(2) ") * (3-CRoot(2) * zeta) by F, FIELD_6:16
.= ((3-CRoot(2) ") * 3-CRoot(2)) * zeta
.= (1. F_Complex) * zeta by A3, VECTSP_2:9 ;

now :: thesis: for o being object st o in {3-CRoot(2),zeta} holds
o in the carrier of E

let o be object ; :: thesis: ( o in {3-CRoot(2),zeta} implies b₁ in the carrier of E )
assume o in {3-CRoot(2),zeta} ; :: thesis: b₁ in the carrier of E

per cases then ( o = 3-CRoot(2) or o = zeta ) by TARSKI:def 2;

suppose o = 3-CRoot(2) ; :: thesis: b₁ in the carrier of E

then o = a ;
hence o in the carrier of E ; :: thesis: verum

end;

suppose o = zeta ; :: thesis: b₁ in the carrier of E

hence o in the carrier of E by A4; :: thesis: verum

end;

end;

end;

then {3-CRoot(2),zeta} c= the carrier of E ;
hence {3-CRoot(2),zeta} is Subset of E ; :: thesis: verum

end;

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

end;

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