let X, x0 be set ; :: thesis: for A being Subset of (DiscrWithInfin (X,x0)) holds
( A is closed iff not ( x0 in X & not x0 in A & not A is finite ) )
set T = DiscrWithInfin (X,x0);
let A be Subset of (DiscrWithInfin (X,x0)); :: thesis: ( A is closed iff not ( x0 in X & not x0 in A & not A is finite ) )
A1: ( A is closed iff ( not x0 in A ` or (A `) ` is finite ) ) by Th19;
the carrier of (DiscrWithInfin (X,x0)) = X by Def5;
hence ( A is closed iff not ( x0 in X & not x0 in A & not A is finite ) ) by A1, XBOOLE_0:def 5; :: thesis: verum