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 :: thesis: for A being Subset of Y st A <> D holds
Int A = A \ {d0}

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 :: thesis: not Int A = D

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

end;

then A4: Int A c= D \ P by A1, Th25;
A \ {d0} c= D \ {d0} by A1, XBOOLE_1:33;
then B \ P is open by A1, Th25;
then Int (A \ P) = A \ P by TOPS_1:23;
then A5: A \ {d0} c= Int A by TOPS_1:19, XBOOLE_1:36;
Int A c= A by TOPS_1:16;
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 :: thesis: for A being Subset of Y holds
( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) )

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 :: thesis: not A = D

D /\ {d0} = {d0} by ZFMISC_1:46;
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:23;
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, Th25; :: thesis: verum