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

proof

assume A3: A = {d0} ; :: thesis:
hence A is closed by Th20; :: thesis:

A4: now :: thesis:

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;

Int A c= A by TOPS_1:16;
then ( Int A = {} or Int A = A ) by A3, ZFMISC_1:33;
hence A is boundary by A4, TOPS_1:48; :: thesis:

end;

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

proof

set Z = A \ {d0};
assume that
A7: not A is empty and
A8: A is closed ; :: thesis:
A9: {d0} c= A by A7, A8, Th20;
A10: A \ {d0} c= A by XBOOLE_1:36;
reconsider Z = A \ {d0} as Subset of (STS (D,d0)) ;
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 A11: Z is open ;
assume A is boundary ; :: thesis:
then A12: Int A = {} ;
assume A13: A <> {d0} ; :: thesis:

now :: thesis:

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

end;

hence contradiction by A10, A12, A11, TOPS_1:24, XBOOLE_1:3; :: thesis:

end;