reconsider t = sqrt 2 as Element of F_Real by XREAL_0:def 1;
not t is zero by SQUARE_1:24;
hence sqrt 2 is non zero Element of F_Real ; :: thesis: verum