let D be non empty set ; :: thesis: for d0 being Element of D st not D \ {d0} is empty holds
for A being Subset of (STS (D,d0)) holds
( ( A = {d0} implies ( A is closed & A is boundary ) ) & ( not A is empty & A is closed & A is boundary implies A = {d0} ) )
let d0 be Element of D; :: thesis: ( not D \ {d0} is empty implies for A being Subset of (STS (D,d0)) holds
( ( A = {d0} implies ( A is closed & A is boundary ) ) & ( not A is empty & A is closed & A is boundary implies A = {d0} ) ) )
assume A1: not D \ {d0} is empty ; :: thesis: for A being Subset of (STS (D,d0)) holds
( ( A = {d0} implies ( A is closed & A is boundary ) ) & ( not A is empty & A is closed & A is boundary implies A = {d0} ) )
set G = { P where P is Subset of D : ( d0 in P & P <> D ) } ;
let A be Subset of (STS (D,d0)); :: thesis: ( ( A = {d0} implies ( A is closed & A is boundary ) ) & ( not A is empty & A is closed & A is boundary implies A = {d0} ) )
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: ( not A is empty & A is closed & A is boundary implies A = {d0} )

proof

assume A3: A = {d0} ; :: thesis: ( A is closed & A is boundary )
hence A is closed by Th20; :: thesis: A is boundary

A4: now :: thesis: not Int A = A

assume A5: Int A = A ; :: thesis: contradiction
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: verum

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

end;

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

proof

set Z = A \ {d0};
assume that
A7: not A is empty and
A8: A is closed ; :: thesis: ( not A is boundary or A = {d0} )
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: A = {d0}
then A12: Int A = {} ;
assume A13: A <> {d0} ; :: thesis: contradiction

now :: thesis: not Z = {}

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

end;

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

end;