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