let X, x0 be set ; :: thesis: ( not X is finite implies for U being Subset of (DiscrWithInfin X,x0) st U = {x0} holds
not U is open )
set T = DiscrWithInfin X,x0;
assume A1: not X is finite ; :: thesis: for U being Subset of (DiscrWithInfin X,x0) st U = {x0} holds
not U is open
let U be Subset of (DiscrWithInfin X,x0); :: thesis: ( U = {x0} implies not U is open )
assume A2: U = {x0} ; :: thesis: not U is open
the carrier of (DiscrWithInfin X,x0) = X by Def5;
then X = (U ` ) \/ {x0} by A2, XBOOLE_1:45;
then A3: not U ` is finite by A1;
x0 in U by A2, TARSKI:def 1;
hence not U is open by A3, Th21; :: thesis: verum