:: deftheorem defines axiom_U2 UNIFORM2:def 10 :
for US being UniformSpaceStr holds
( US is axiom_U2 iff for S being Element of the entourages of US holds S [~] in the entourages of US );