theorem Th41: :: RUSUB_5:41

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