theorem :: FIELD_10:32

{1,(sqrt 2)} is Basis of (VecSp ((FAdj (F_Rat,{2-Root(2)})),F_Rat))