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;
A1: the carrier of (DiscrWithInfin X,x0) = X by Def5;
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 ) )
( A is closed iff A ` is open ) by TOPS_1:29;
then ( A is closed iff ( not x0 in A ` or (A ` ) ` is finite ) ) by Th21;
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