:: deftheorem defines axiom_UL UNIFORM2:def 18 :
for SUS being non empty Semi-UniformSpace holds
( SUS is axiom_UL iff for S being Element of the entourages of SUS
for x being Element of SUS ex W being Element of the entourages of SUS st { y where y is Element of SUS : [x,y] in W [*] W } c= Neighborhood (S,x) );