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

now :: thesis: for A being Subset of X holds A is open

let A be Subset of X; :: thesis: A is open
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: ( not x in { B where B is Subset of X : ex a being Point of X st
( a in A & B = {a} ) } or x in bool A )
assume x in { B where B is Subset of X : ex a being Point of X st
( a in A & B = {a} ) } ; :: thesis: x in bool A
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: 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 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: 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 A6: 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 A7: y in P ; :: thesis: y in union F
then reconsider a = y as Point of X ;

now :: thesis: ex B0 being set st
( y in B0 & B0 in F )

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

end;

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

end;

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

end;

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

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

let B be Subset of X; :: thesis: ( B in F implies B is open )
assume B in F ; :: thesis: B is open
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: verum

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: verum

end;

hence X is discrete by Th15; :: thesis: verum