theorem :: TEX_2:17

for Y being non empty TopStruct
for Y0 being 1 -element SubSpace of Y ex y being Point of Y st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of (Sspace y), the topology of (Sspace y) #)