let X be TopSpace; :: thesis:
assume A1: for A being Subset of X
for x being Point of X st A = {x} holds
A is open ; :: thesis:

now :: thesis:

let A be Subset of X; :: thesis:
set F = { B where B is Subset of X : ex a being Point of X st
( a in A & B = {a} ) } ;
A2: { B where B is Subset of X : ex a being Point of X st
( a in A & B = {a} ) } c= bool A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { B where B is Subset of X : ex a being Point of X st
( a in A & B = {a} ) } ; :: thesis:
then consider C being Subset of X such that
A3: x = C and
A4: ex a being Point of X st
( a in A & C = {a} ) ;
C c= A by A4, ZFMISC_1:31;
hence x in bool A by A3; :: thesis:

end;

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

now :: thesis:

let x be set ; :: thesis:
assume A6: x in bool A ; :: thesis:
then reconsider P = x as Subset of X by XBOOLE_1:1;

now :: thesis:

let y be object ; :: thesis:
assume A7: y in P ; :: thesis:
then reconsider a = y as Point of X ;

now :: thesis:

take B0 = {a}; :: thesis:
B0 is Subset of X by A7, ZFMISC_1:31;
hence ( y in B0 & B0 in F ) by A6, A7, TARSKI:def 1; :: thesis:

end;

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

end;

hence x c= union F ; :: thesis:

end;

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

now :: thesis:

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

end;

then A9: F is open by TOPS_2:def 1;
union F c= union (bool A) by A2, ZFMISC_1:77;
then union F = A by A8, A5;
hence A is open by A9, TOPS_2:19; :: thesis:

end;

hence X is discrete by Th15; :: thesis: