let D be non empty set ; :: thesis:
let d0 be Element of D; :: thesis:
assume A1: not D \ {d0} is empty ; :: thesis:
let A be Subset of (STS D,d0); :: thesis:
set G = { P where P is Subset of D : ( d0 in P & P <> D ) } ;
A2: Int A in the topology of (STS D,d0) by PRE_TOPC:def 5;
thus ( A = {d0} implies ( A is closed & A is boundary ) ) :: thesis:

assume A3: A = {d0} ; :: thesis:
hence A is closed by Th24; :: thesis:
Int A c= A by TOPS_1:44;
then A4: ( Int A = {} or Int A = A ) by A3, ZFMISC_1:39;

assume A5: Int A = A ; :: thesis:
then A6: d0 in Int A by A3, TARSKI:def 1;
Int A <> D by A1, A3, A5, XBOOLE_1:37;
then Int A in { P where P is Subset of D : ( d0 in P & P <> D ) } by A6;
hence contradiction by A2, XBOOLE_0:def 5; :: thesis:

end;

hence A is boundary by A4, TOPS_1:84; :: thesis:

end;

thus ( not A is empty & A is closed & A is boundary implies A = {d0} ) :: thesis:

assume ( not A is empty & A is closed ) ; :: thesis:
then A7: {d0} c= A by Th24;
set Z = A \ {d0};
A8: A \ {d0} c= A by XBOOLE_1:36;
reconsider Z = A \ {d0} as Subset of (STS D,d0) ;
assume A is boundary ; :: thesis:
then A9: Int A = {} ;
assume A10: A <> {d0} ; :: thesis:

A11: now

assume Z = {} ; :: thesis:
then A c= {d0} by XBOOLE_1:37;
hence contradiction by A7, A10, XBOOLE_0:def 10; :: thesis:

end;

d0 in {d0} by TARSKI:def 1;
then for Q being Subset of D holds
( not Q = Z or not d0 in Q or not Q <> D ) by XBOOLE_0:def 5;
then not Z in { P where P is Subset of D : ( d0 in P & P <> D ) } ;
then Z in the topology of (STS D,d0) by XBOOLE_0:def 5;
then Z is open by PRE_TOPC:def 5;
hence contradiction by A8, A9, A11, TOPS_1:56, XBOOLE_1:3; :: thesis:

end;