for Y being TopStruct
for Y0 being SubSpace of Y
for F being Subset of Y st F is closed holds
ex F0 being Subset of Y0 st
( F0 is closed & F0 = F /\ the carrier of Y0 )