:: deftheorem defines TopUnitSpace RUSUB_5:def 6 :
for V being RealUnitarySpace holds TopUnitSpace V = TopStruct(# the carrier of V,(Family_open_set V) #);