for V being RealUnitarySpace holds
( the carrier of V = the carrier of (TopUnitSpace V) & the topology of (TopUnitSpace V) = Family_open_set V ) ;