set E = FAdj (F_Rat,{3-Root(2)});
set p = X^3-2 ;
H: ( {3-Root(2)} is Subset of (FAdj (F_Rat,{3-Root(2)})) & 3-Root(2) in {3-Root(2)} ) by FIELD_6:35, TARSKI:def 1;
{3-Root(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_10:64, FIELD_4:def 4;
then consider a being Element of (FAdj (F_Rat,{3-Root(2)})) such that
A: ( a = 3-Root(2) & a is_a_root_of X^3-2 , FAdj (F_Rat,{3-Root(2)}) ) by H;
thus not FAdj (F_Rat,{3-Root(2)}) is F_Rat -normal by A, FIELD_4:def 3, FIELD_10:65; :: thesis: verum