let X, x0 be set ; :: thesis: ( X is infinite implies for U being Subset of (DiscrWithInfin (X,x0)) st U = {x0} holds
not U is open )
set T = DiscrWithInfin (X,x0);
assume A1: X is infinite ; :: 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: U ` is infinite by A1;
x0 in U by A2, TARSKI:def 1;
hence not U is open by A3, Th19; :: thesis: verum