theorem :: UNIFORM3:13

for US being UniformSpace holds US is axiom_U3 Semi-UniformSpace ;