let USS be non empty cap-closed axiom_U1 UniformSpaceStr ; :: thesis: for x being Element of USS
for V, W being Element of the entourages of USS holds (Neighborhood (V,x)) /\ (Neighborhood (W,x)) = Neighborhood ((V /\ W),x)
let x be Element of USS; :: thesis: for V, W being Element of the entourages of USS holds (Neighborhood (V,x)) /\ (Neighborhood (W,x)) = Neighborhood ((V /\ W),x)
let V, W be Element of the entourages of USS; :: thesis: (Neighborhood (V,x)) /\ (Neighborhood (W,x)) = Neighborhood ((V /\ W),x)
set NV = Neighborhood (V,x);
set NW = Neighborhood (W,x);
set NVW = Neighborhood ((V /\ W),x);
A1: (Neighborhood (V,x)) /\ (Neighborhood (W,x)) c= Neighborhood ((V /\ W),x)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in (Neighborhood (V,x)) /\ (Neighborhood (W,x)) or t in Neighborhood ((V /\ W),x) )
assume A2: t in (Neighborhood (V,x)) /\ (Neighborhood (W,x)) ; :: thesis: t in Neighborhood ((V /\ W),x)
then t in { y where y is Element of USS : [x,y] in V } by XBOOLE_0:def 4;
then consider y1 being Element of USS such that
A3: t = y1 and
A4: [x,y1] in V ;
t in { y where y is Element of USS : [x,y] in W } by A2, XBOOLE_0:def 4;
then consider y2 being Element of USS such that
A5: t = y2 and
A6: [x,y2] in W ;
( [x,y1] in V /\ W & [x,y2] in V /\ W ) by A3, A4, A5, A6, XBOOLE_0:def 4;
hence t in Neighborhood ((V /\ W),x) by A3; :: thesis: verum

end;

Neighborhood ((V /\ W),x) c= (Neighborhood (V,x)) /\ (Neighborhood (W,x))

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in Neighborhood ((V /\ W),x) or t in (Neighborhood (V,x)) /\ (Neighborhood (W,x)) )
assume t in Neighborhood ((V /\ W),x) ; :: thesis: t in (Neighborhood (V,x)) /\ (Neighborhood (W,x))
then consider y being Element of USS such that
A7: t = y and
A8: [x,y] in V /\ W ;
A9: ( [x,y] in V & [x,y] in W ) by A8, XBOOLE_0:def 4;
then A10: t in Neighborhood (V,x) by A7;
t in { y where y is Element of USS : [x,y] in W } by A7, A9;
hence t in (Neighborhood (V,x)) /\ (Neighborhood (W,x)) by A10, XBOOLE_0:def 4; :: thesis: verum

end;

hence (Neighborhood (V,x)) /\ (Neighborhood (W,x)) = Neighborhood ((V /\ W),x) by A1; :: thesis: verum