set F = FAdj (F_Rat,{3-CRoot(2),zeta});
set K = FAdj (F_Rat,{2-CRoot(2),zeta});

now :: thesis: sqrt 2 is not Element of (FAdj (F_Rat,{3-CRoot(2),zeta}))

assume sqrt 2 is Element of (FAdj (F_Rat,{3-CRoot(2),zeta})) ; :: thesis: contradiction
then reconsider a = sqrt 2 as Element of (FAdj (F_Rat,{3-CRoot(2),zeta})) ;
{a} is Subset of (FAdj (F_Rat,{3-CRoot(2),zeta})) ;
then FAdj (F_Rat,{3-CRoot(2),zeta}) = FAdj ((FAdj (F_Rat,{3-CRoot(2),zeta})),{2-CRoot(2)}) by FIELD_7:2, FIELD_7:3
.= FAdj (F_Rat,({3-CRoot(2),zeta} \/ {2-CRoot(2)})) by FIELD_7:34
.= FAdj (F_Rat,{3-CRoot(2),zeta,2-CRoot(2)}) by ENUMSET1:3 ;
then C: 6 = (deg ((FAdj (F_Rat,{3-CRoot(2),zeta,2-CRoot(2)})),(FAdj (F_Rat,{2-CRoot(2),zeta})))) * 4 by grad4, grad6, FIELD_7:30;

now :: thesis: for n being Integer
for k being Nat st k <> 0 & 3 / 2 = n / k holds
2 <= k

let n be Integer; :: thesis: for k being Nat st k <> 0 & 3 / 2 = n / k holds
2 <= k
let k be Nat; :: thesis: ( k <> 0 & 3 / 2 = n / k implies 2 <= k )
assume C3: ( k <> 0 & 3 / 2 = n / k ) ; :: thesis: 2 <= k
then (3 / 2) * k = (n / k) * k
.= (n * k) * (k ")
.= n by C3, XCMPLX_1:203 ;
then C4: 3 * k = n * 2 ;
C5: 3 = (2 * 1) + 1 ;

now :: thesis: not 2 > k

assume 2 > k ; :: thesis: contradiction
then k is trivial by NAT_2:29;

per cases then ( k = 0 or k = 1 ) by NAT_2:def 1;

suppose k = 0 ; :: thesis: contradiction

hence contradiction by C3; :: thesis: verum

end;

suppose k = 1 ; :: thesis: contradiction

hence contradiction by C5, C4; :: thesis: verum

end;

end;

end;

hence 2 <= k ; :: thesis: verum

end;

then denominator (3 / 2) = 2 by RAT_1:def 3;
hence contradiction by C, RAT_1:21; :: thesis: verum

end;

hence sqrt 2 is not Element of (FAdj (F_Rat,{3-CRoot(2),zeta})) ; :: thesis: verum