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;
assume that
A1: x in X and
A2: x <> x0 ; :: thesis: {x} is open Subset of (DiscrWithInfin X,x0)
A3: the carrier of (DiscrWithInfin X,x0) = X by Def5;
not x0 in {x} by A2, TARSKI:def 1;
hence {x} is open Subset of (DiscrWithInfin X,x0) by A3, A1, Th21, ZFMISC_1:37; :: thesis: verum