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

( x = 0 & [0,0] in SinglRel 0 ) by TARSKI:def 1;

hence x in U_FT x by RELAT_1:def 13; :: thesis: verum