reconsider t = 3 -Root 2 as Element of F_Real by XREAL_0:def 1;
not t is zero ;
hence 3 -Root 2 is non zero Element of F_Real ; :: thesis: verum