theorem :: FINTOPO7:21

for ET being FMT_TopSpace
for B being Basis of ET holds Family_open_set ET = UniCl B