theorem bas3R: :: FIELD_10:61

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