for V being RealUnitarySpace holds the carrier of V in Family_open_set V