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, Def5;
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, Def5;
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, XBOOLE_1:1;
Ball z,q c= Ball z,p by Th1, XXREAL_0:17;
then Ball z,q c= V by A5, XBOOLE_1:1;
hence Ball z,q c= V /\ W by A8, XBOOLE_1:19; :: thesis: verum

end;

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