:: deftheorem defines fundamental_element_of_entourages UNIFORM3:def 2 :
for MS being non empty MetrStruct
for r being positive Real holds fundamental_element_of_entourages (MS,r) = { [x,y] where x, y is Element of MS : dist (x,y) <= r } ;