theorem Th11bis: :: UNIFORM2:18

for X being set
for cB being Subset-Family of [:X,X:] st cB is quasi_basis & cB is axiom_UP1 & cB is axiom_UP3 holds
UniformSpaceStr(# X,<.cB.] #) is Quasi-UniformSpace