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 z in V /\ W ; :: thesis: ex q being Real st
( q > 0 & Ball z,q c= V /\ W )
then A3: ( z in V & z in W ) by XBOOLE_0:def 4;
then consider p being Real such that
A4: ( p > 0 & Ball z,p c= V ) by A1, Def5;
consider r being Real such that
A5: ( r > 0 & Ball z,r c= W ) by A2, A3, Def5;
take q = min p,r; :: thesis: ( q > 0 & Ball z,q c= V /\ W )
A6: ( q <= p & q > 0 ) by A4, A5, XXREAL_0:15, XXREAL_0:17;
thus q > 0 by A4, A5, XXREAL_0:15; :: thesis: Ball z,q c= V /\ W
Ball z,q c= Ball z,p by A6, Th1;
then A7: Ball z,q c= V by A4, XBOOLE_1:1;
( q <= r & q > 0 ) by A4, A5, XXREAL_0:15, XXREAL_0:17;
then Ball z,q c= Ball z,r by Th1;
then Ball z,q c= W by A5, XBOOLE_1:1;
hence Ball z,q c= V /\ W by A7, XBOOLE_1:19; :: thesis: verum

end;

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