theorem :: UNIFORM3:12

for US being UniformSpace holds US is axiom_U2 Quasi-UniformSpace ;