:: deftheorem defines [~] UNIFORM2:def 6 :
for US being UniformSpaceStr holds US [~] = UniformSpaceStr(# the carrier of US,( the entourages of US [~]) #);