:: deftheorem defines @ UNIFORM3:def 22 :
for US being non empty UniformSpace holds @ US = US;