theorem Th7: :: UNIFORM3:16

for X being set
for cB being Subset-Family of [:X,X:] st cB is quasi_basis & cB is axiom_UP1 & cB is axiom_UP2 & cB is axiom_UP3 holds
ex US being strict UniformSpace st
( the carrier of US = X & the entourages of US = <.cB.] )