for V being RealUnitarySpace
for A being Subset-Family of V st A c= Family_open_set V holds
union A in Family_open_set V