for V being RealUnitarySpace holds TopStruct(# the carrier of V,(Family_open_set V) #) is TopSpace