for Y being non empty TopStruct
for Y0 being non proper SubSpace of Y holds TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y, the topology of Y #)