:: deftheorem defines axiom_U3 UNIFORM2:def 11 :
for US being UniformSpaceStr holds
( US is axiom_U3 iff for S being Element of the entourages of US ex W being Element of the entourages of US st W [*] W c= S );