let X, x0, x be set ; :: thesis: ( x in X implies {x} is closed Subset of (DiscrWithInfin X,x0) )
set T = DiscrWithInfin X,x0;
the carrier of (DiscrWithInfin X,x0) = X by Def5;
hence ( x in X implies {x} is closed Subset of (DiscrWithInfin X,x0) ) by Th22, ZFMISC_1:37; :: thesis: verum