:: deftheorem defines upper UNIFORM2:def 7 :
for US being UniformSpaceStr holds
( US is upper iff the entourages of US is upper );