theorem :: UNIFORM3:56

for US being UniformSpaceStr holds
( the carrier of (RelStr2UniformSpaceStr (UniformSpaceStr2RelStr US)) = the carrier of US & the entourages of (RelStr2UniformSpaceStr (UniformSpaceStr2RelStr US)) = rho (meet the entourages of US) ) ;