set K = FAdj (F_Rat,{3-CRoot(2)});
the carrier of (Polynom-Ring F_Rat) c= the carrier of (Polynom-Ring (FAdj (F_Rat,{3-CRoot(2)}))) by FIELD_4:10;
then reconsider p = X^2+X+1 as Element of the carrier of (Polynom-Ring (FAdj (F_Rat,{3-CRoot(2)}))) ;
deg p = 2 by LL, FIELD_4:20;
then reconsider p = p as non constant Element of the carrier of (Polynom-Ring (FAdj (F_Rat,{3-CRoot(2)}))) by RING_4:def 4;
H: Roots (F_Complex,X^2+X+1) = { a where a is Element of F_Complex : a is_a_root_of X^2+X+1 , F_Complex } by FIELD_4:def 4;
zeta in Roots (F_Complex,X^2+X+1) by rootz, TARSKI:def 2;
then consider a being Element of F_Complex such that
I: ( a = zeta & a is_a_root_of X^2+X+1 , F_Complex ) by H;
0. F_Complex = Ext_eval (X^2+X+1,zeta) by I, FIELD_4:def 2
.= Ext_eval (p,zeta) by FIELD_8:6 ;
hence zeta is FAdj (F_Rat,{3-CRoot(2)}) -algebraic by FIELD_6:43; :: thesis: verum