theorem Th59: :: TOPGEN_4:59
for T being non empty TopSpace
for F, G being Subset-Family of T st F is all-open-containing & F c= G holds
G is all-open-containing ;