theorem Th9: :: FINTOPO7:14

for ET being FMT_TopSpace holds
( {} in Family_open_set ET & the carrier of ET in Family_open_set ET & ( for a being Subset-Family of ET st a c= Family_open_set ET holds
union a in Family_open_set ET ) & ( for a, b being Subset of ET st a in Family_open_set ET & b in Family_open_set ET holds
a /\ b in Family_open_set ET ) )