theorem :: TOPS_2:12

for T being TopStruct
for F, G being Subset-Family of T st F c= G & G is closed holds
F is closed ;