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 )
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 ) } ;
A2: union (bool A) = A by ZFMISC_1:81;
assume A3: A is closed ; :: thesis: A is open
A4: 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 that
A5: a in A and
A6: C = {a} ; :: thesis: Cl C c= A
C c= A by A5, A6, ZFMISC_1:31;
then Cl C c= Cl A by PRE_TOPC:19;
hence Cl C c= A by A3, PRE_TOPC:22; :: thesis: verum

end;

A7: { 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 object ; :: 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
A8: x = P and
A9: 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 A4, A9;
hence x in bool A by A8; :: thesis: verum

end;

bool A c= bool the carrier of X by ZFMISC_1:67;
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 A7, XBOOLE_1:1;

now :: thesis: for x being set st x in bool A holds
x c= union F

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

now :: thesis: for y being object st y in P holds
y in union F

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

now :: thesis: ex B being Element of K10( the carrier of X) st
( y in B & B in F )

reconsider P0 = {a} as Subset of X by A11, ZFMISC_1:31;
take B = Cl P0; :: thesis: ( y in B & B in F )
A12: P0 c= B by PRE_TOPC:18;
a in P0 by TARSKI:def 1;
hence ( y in B & B in F ) by A10, A11, A12; :: thesis: verum

end;

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

end;

hence x c= union F ; :: thesis: verum

end;

then A13: union (bool A) c= union F ;

now :: thesis: for D being Subset of X st D in F holds
D is open

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 A14: F is open by TOPS_2:def 1;
union F c= union (bool A) by A7, ZFMISC_1:77;
then union F = A by A13, A2;
hence A is open by A14, TOPS_2:19; :: thesis: verum

end;

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