let D be non empty set ; 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 non empty Subset of Y holds Cl A = A \/ {d0} ) ) )
let d0 be 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 non empty Subset of Y holds Cl A = A \/ {d0} ) ) )
let Y be non empty TopSpace; ( 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 non empty Subset of Y holds Cl 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 non empty Subset of Y holds Cl A = A \/ {d0} ) ) )
( the carrier of Y = D & ( for A being non empty Subset of Y holds Cl 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)) #) )
assume A5:
the carrier of Y = D
; ( ex A being non empty Subset of Y st not Cl 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 A6:
for A being non empty Subset of Y holds Cl A = A \/ {d0}
; TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #)
hence
TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #)
by A5, Th24; verum