let PM be MetrStruct ; 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; ( 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
; 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;
( z in V /\ W implies ex q being Real st
( q > 0 & Ball (z,q) c= V /\ W ) )
assume A3:
z in V /\ W
;
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);
( q > 0 & Ball (z,q) c= V /\ W )
thus
q > 0
by A4, A6, XXREAL_0:15;
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;
verum
end;
hence
V /\ W in Family_open_set PM
by Def4; verum