theorem :: TOPS_2:27

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