reconsider t = 3 -Root 2 as Element of F_Real by XREAL_0:def 1;
B: F_Real is Subfield of F_Complex by FIELD_4:7;
then the carrier of F_Real c= the carrier of F_Complex by EC_PF_1:def 1;
then reconsider t = t as Element of F_Complex ;
3 -Root 2 <> 0. F_Real ;
then not t is zero by B, EC_PF_1:def 1;
hence 3 -Root 2 is non zero Element of F_Complex ; :: thesis: verum