:: deftheorem defines fundamental_system_of_entourages UNIFORM3:def 3 :
for MS being non empty MetrStruct holds fundamental_system_of_entourages MS = { (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } ;