FAdj (F_Rat,{3-CRoot(2),zeta,2-CRoot(2)}) = FAdj (F_Rat,{zeta,2-CRoot(2),3-CRoot(2)}) by ENUMSET1:59
.= FAdj (F_Rat,({zeta,2-CRoot(2)} \/ {3-CRoot(2)})) by ENUMSET1:3
.= FAdj ((FAdj (F_Rat,{2-CRoot(2),zeta})),{3-CRoot(2)}) by FIELD_7:34 ;
hence FAdj (F_Rat,{3-CRoot(2),zeta,2-CRoot(2)}) is FAdj (F_Rat,{2-CRoot(2),zeta}) -finite ; :: thesis: verum