theorem :: TOPS_2:11

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