:: deftheorem defines RelStr2UniformSpaceStr UNIFORM3:def 26 :
for RS being RelStr holds RelStr2UniformSpaceStr RS = UniformSpaceStr(# the carrier of RS,(InternalRel2Uniformity RS) #);