let X be TopSpace; :: thesis: ( ( for A being Subset of X
for x being Point of X st A = {x} holds
Cl A is open ) implies X is almost_discrete )
assume A1: for D being Subset of X
for x being Point of X st D = {x} holds
Cl D is open ; :: thesis: X is almost_discrete
for A being Subset of X st A is closed holds
A is open

proof

let A be Subset of X; :: thesis: ( A is closed implies A is open )
assume A2: A is closed ; :: thesis: A is open
A3: for C being Subset of X
for a being Point of X st a in A & C = {a} holds
Cl C c= A

proof

let C be Subset of X; :: thesis: for a being Point of X st a in A & C = {a} holds
Cl C c= A
let a be Point of X; :: thesis: ( a in A & C = {a} implies Cl C c= A )
assume ( a in A & C = {a} ) ; :: thesis: Cl C c= A
then C c= A by ZFMISC_1:37;
then Cl C c= Cl A by PRE_TOPC:49;
hence Cl C c= A by A2, PRE_TOPC:52; :: thesis: verum

end;

set F = { B where B is Subset of X : ex C being Subset of X ex a being Point of X st
( a in A & C = {a} & B = Cl C ) } ;
A4: { B where B is Subset of X : ex C being Subset of X ex a being Point of X st
( a in A & C = {a} & B = Cl C ) } c= bool A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { B where B is Subset of X : ex C being Subset of X ex a being Point of X st
( a in A & C = {a} & B = Cl C ) } or x in bool A )
assume x in { B where B is Subset of X : ex C being Subset of X ex a being Point of X st
( a in A & C = {a} & B = Cl C ) } ; :: thesis: x in bool A
then consider P being Subset of X such that
A5: x = P and
A6: ex C being Subset of X ex a being Point of X st
( a in A & C = {a} & P = Cl C ) ;
P c= A by A3, A6;
hence x in bool A by A5; :: thesis: verum

end;

bool A c= bool the carrier of X by ZFMISC_1:79;
then reconsider F = { B where B is Subset of X : ex C being Subset of X ex a being Point of X st
( a in A & C = {a} & B = Cl C ) } as Subset-Family of X by A4, XBOOLE_1:1;

now

let D be Subset of X; :: thesis: ( D in F implies D is open )
assume D in F ; :: thesis: D is open
then ex S being Subset of X st
( S = D & ex C being Subset of X ex a being Point of X st
( a in A & C = {a} & S = Cl C ) ) ;
hence D is open by A1; :: thesis: verum

end;

then A7: F is open by TOPS_2:def 1;

now

let x be set ; :: thesis: ( x in bool A implies x c= union F )
assume A8: x in bool A ; :: thesis: x c= union F
then reconsider P = x as Subset of X by XBOOLE_1:1;

now

let y be set ; :: thesis: ( y in P implies y in union F )
assume A9: y in P ; :: thesis: y in union F
then reconsider a = y as Point of X ;

now

reconsider P0 = {a} as Subset of X by A9, ZFMISC_1:37;
take B = Cl P0; :: thesis: ( y in B & B in F )
( a in P0 & P0 c= B ) by PRE_TOPC:48, TARSKI:def 1;
hence ( y in B & B in F ) by A8, A9; :: thesis: verum

end;

hence y in union F by TARSKI:def 4; :: thesis: verum

end;

hence x c= union F by TARSKI:def 3; :: thesis: verum

end;

then ( union (bool A) c= union F & union F c= union (bool A) & union (bool A) = A ) by A4, ZFMISC_1:95, ZFMISC_1:99;
then union F = A by XBOOLE_0:def 10;
hence A is open by A7, TOPS_2:26; :: thesis: verum

end;

hence X is almost_discrete by Th24; :: thesis: verum