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 Th20, ZFMISC_1:31; :: thesis: verum