:: deftheorem defines UniformSpaceStr2RelStr UNIFORM3:def 24 :
for USS being UniformSpaceStr holds UniformSpaceStr2RelStr USS = RelStr(# the carrier of USS,(Uniformity2InternalRel USS) #);