theorem :: TOPS_2:28

for T being TopStruct
for F being Subset-Family of T
for A being SubSpace of T st F is closed holds
for G being Subset-Family of A st G = F holds
G is closed by Th26;