:: deftheorem defines axiom_U1 UNIFORM2:def 9 :
for US being UniformSpaceStr holds
( US is axiom_U1 iff for S being Element of the entourages of US holds id the carrier of US c= S );