let x be Element of FT{0} ; :: according to FIN_TOPO:def 4 :: thesis: x in U_FT x
A1: x = 0 by TARSKI:def 1;
[0 ,0 ] in SinglRel 0 by TARSKI:def 1;
hence x in U_FT x by A1, RELAT_1:def 13; :: thesis: verum