take the non empty axiom_U3 Semi-UniformSpace ; :: thesis: the non empty axiom_U3 Semi-UniformSpace is axiom_UL
thus the non empty axiom_U3 Semi-UniformSpace is axiom_UL ; :: thesis: verum