let X, x0, x be set ; :: thesis: ( x in X & x <> x0 implies {x} is open Subset of (DiscrWithInfin X,x0) )
set T = DiscrWithInfin X,x0;
A1: the carrier of (DiscrWithInfin X,x0) = X by Def5;
assume ( x in X & x <> x0 ) ; :: thesis: {x} is open Subset of (DiscrWithInfin X,x0)
then ( {x} c= the carrier of (DiscrWithInfin X,x0) & not x0 in {x} ) by A1, TARSKI:def 1, ZFMISC_1:37;
hence {x} is open Subset of (DiscrWithInfin X,x0) by Th21; :: thesis: verum