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