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