:: deftheorem defines uniformity_induced_by UNIFORM3:def 21 :
for X being set
for R being Relation of X holds uniformity_induced_by R = UniformSpaceStr(# X,(rho R) #);