for Y being TopStruct
for Y0 being SubSpace of Y
for G being Subset of Y st G is open holds
ex G0 being Subset of Y0 st
( G0 is open & G0 = G /\ the carrier of Y0 )