let D be non empty set ; :: thesis: for d0 being Element of D
for Y being non empty TopSpace holds
( TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of (STS D,d0),the topology of (STS D,d0) #) iff ( the carrier of Y = D & ( for A being Subset of Y st A <> D holds
Int A = A \ {d0} ) ) )
let d0 be Element of D; :: thesis: for Y being non empty TopSpace holds
( TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of (STS D,d0),the topology of (STS D,d0) #) iff ( the carrier of Y = D & ( for A being Subset of Y st A <> D holds
Int A = A \ {d0} ) ) )
let Y be non empty TopSpace; :: thesis: ( TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of (STS D,d0),the topology of (STS D,d0) #) iff ( the carrier of Y = D & ( for A being Subset of Y st A <> D holds
Int A = A \ {d0} ) ) )
thus ( TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of (STS D,d0),the topology of (STS D,d0) #) implies ( the carrier of Y = D & ( for A being Subset of Y st A <> D holds
Int A = A \ {d0} ) ) ) :: thesis: ( the carrier of Y = D & ( for A being Subset of Y st A <> D holds
Int A = A \ {d0} ) implies TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of (STS D,d0),the topology of (STS D,d0) #) )

proof

assume A1: TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of (STS D,d0),the topology of (STS D,d0) #) ; :: thesis: ( the carrier of Y = D & ( for A being Subset of Y st A <> D holds
Int A = A \ {d0} ) )
hence the carrier of Y = D ; :: thesis: for A being Subset of Y st A <> D holds
Int A = A \ {d0}
reconsider P = {d0} as Subset of Y by A1;

now

let A be Subset of Y; :: thesis: ( A <> D implies Int A = A \ {d0} )
reconsider B = A as Subset of Y ;
A2: A = A /\ D by A1, XBOOLE_1:28;
assume A3: A <> D ; :: thesis: Int A = A \ {d0}

now

assume Int A = D ; :: thesis: contradiction
then D c= A by TOPS_1:44;
hence contradiction by A1, A3, XBOOLE_0:def 10; :: thesis: verum

end;

then A4: Int A c= D \ P by A1, Th29;
A \ {d0} c= D \ {d0} by A1, XBOOLE_1:33;
then B \ P is open by A1, Th29;
then Int (A \ P) = A \ P by TOPS_1:55;
then A5: A \ {d0} c= Int A by TOPS_1:48, XBOOLE_1:36;
Int A c= A by TOPS_1:44;
then Int A c= A /\ (D \ P) by A4, XBOOLE_1:19;
then Int A c= A \ {d0} by A2, XBOOLE_1:49;
hence Int A = A \ {d0} by A5, XBOOLE_0:def 10; :: thesis: verum

end;

hence for A being Subset of Y st A <> D holds
Int A = A \ {d0} ; :: thesis: verum

end;

assume A6: the carrier of Y = D ; :: thesis: ( ex A being Subset of Y st
( A <> D & not Int A = A \ {d0} ) or TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of (STS D,d0),the topology of (STS D,d0) #) )
assume A7: for A being Subset of Y st A <> D holds
Int A = A \ {d0} ; :: thesis: TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of (STS D,d0),the topology of (STS D,d0) #)

now

let A be Subset of Y; :: thesis: ( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) )
thus ( A c= D \ {d0} implies A is open ) :: thesis: ( A <> D & A is open implies A c= D \ {d0} )

proof

assume A8: A c= D \ {d0} ; :: thesis: A is open

A9: now

D /\ {d0} = {d0} by ZFMISC_1:52;
then A10: D meets {d0} by XBOOLE_0:def 7;
assume A = D ; :: thesis: contradiction
then D = D \ {d0} by A8, XBOOLE_0:def 10;
hence contradiction by A10, XBOOLE_1:83; :: thesis: verum

end;

A11: A = A /\ D by A6, XBOOLE_1:28;
A = A /\ (D \ {d0}) by A8, XBOOLE_1:28;
then A = A \ {d0} by A11, XBOOLE_1:49;
then Int A = A by A7, A9;
hence A is open ; :: thesis: verum

end;

thus ( A <> D & A is open implies A c= D \ {d0} ) :: thesis: verum

proof

assume A12: A <> D ; :: thesis: ( not A is open or A c= D \ {d0} )
assume A is open ; :: thesis: A c= D \ {d0}
then Int A = A by TOPS_1:55;
then A \ {d0} = A by A7, A12;
hence A c= D \ {d0} by A6, XBOOLE_1:33; :: thesis: verum

end;

end;

hence TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of (STS D,d0),the topology of (STS D,d0) #) by A6, Th29; :: thesis: verum