let US be non empty Semi-UniformSpace; :: thesis: ( US is axiom_U3 implies US is axiom_UL )
assume A1: US is axiom_U3 ; :: thesis: US is axiom_UL
let S be Element of the entourages of US; :: according to UNIFORM2:def 18 :: thesis: for x being Element of US ex W being Element of the entourages of US st { y where y is Element of US : [x,y] in W [*] W } c= Neighborhood (S,x)
let x be Element of US; :: thesis: ex W being Element of the entourages of US st { y where y is Element of US : [x,y] in W [*] W } c= Neighborhood (S,x)
consider W being Element of the entourages of US such that
A2: W * W c= S by A1;
{ y where y is Element of US : [x,y] in W * W } c= Neighborhood (S,x)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { y where y is Element of US : [x,y] in W * W } or t in Neighborhood (S,x) )
assume t in { y where y is Element of US : [x,y] in W * W } ; :: thesis: t in Neighborhood (S,x)
then ex y0 being Element of US st
( t = y0 & [x,y0] in W * W ) ;
hence t in Neighborhood (S,x) by A2; :: thesis: verum

end;

hence ex W being Element of the entourages of US st { y where y is Element of US : [x,y] in W [*] W } c= Neighborhood (S,x) ; :: thesis: verum