theorem Th38: :: RUSUB_5:38

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