let PM be MetrStruct ; :: thesis: for V, W being Subset of PM st V in Family_open_set PM & W in Family_open_set PM holds
V /\ W in Family_open_set PM
let V, W be Subset of PM; :: thesis: ( V in Family_open_set PM & W in Family_open_set PM implies V /\ W in Family_open_set PM )
assume that
A1: V in Family_open_set PM and
A2: W in Family_open_set PM ; :: thesis: V /\ W in Family_open_set PM
for z being Element of PM st z in V /\ W holds
ex q being Real st
( q > 0 & Ball (z,q) c= V /\ W )

proof

let z be Element of PM; :: thesis: ( z in V /\ W implies ex q being Real st
( q > 0 & Ball (z,q) c= V /\ W ) )
assume A3: z in V /\ W ; :: thesis: ex q being Real st
( q > 0 & Ball (z,q) c= V /\ W )
then z in V by XBOOLE_0:def 4;
then consider p being Real such that
A4: p > 0 and
A5: Ball (z,p) c= V by A1, Def4;
z in W by A3, XBOOLE_0:def 4;
then consider r being Real such that
A6: r > 0 and
A7: Ball (z,r) c= W by A2, Def4;
take q = min (p,r); :: thesis: ( q > 0 & Ball (z,q) c= V /\ W )
thus q > 0 by A4, A6, XXREAL_0:15; :: thesis: Ball (z,q) c= V /\ W
Ball (z,q) c= Ball (z,r) by Th1, XXREAL_0:17;
then A8: Ball (z,q) c= W by A7;
Ball (z,q) c= Ball (z,p) by Th1, XXREAL_0:17;
then Ball (z,q) c= V by A5;
hence Ball (z,q) c= V /\ W by A8, XBOOLE_1:19; :: thesis: verum

end;

hence V /\ W in Family_open_set PM by Def4; :: thesis: verum