let V be RealUnitarySpace; for M, N being Subset of V st M in Family_open_set V & N in Family_open_set V holds
M /\ N in Family_open_set V
let M, N be Subset of V; ( M in Family_open_set V & N in Family_open_set V implies M /\ N in Family_open_set V )
assume that
A1:
M in Family_open_set V
and
A2:
N in Family_open_set V
; M /\ N in Family_open_set V
for v being Point of V st v in M /\ N holds
ex q being Real st
( q > 0 & Ball (v,q) c= M /\ N )
proof
let v be
Point of
V;
( v in M /\ N implies ex q being Real st
( q > 0 & Ball (v,q) c= M /\ N ) )
assume A3:
v in M /\ N
;
ex q being Real st
( q > 0 & Ball (v,q) c= M /\ N )
then
v in M
by XBOOLE_0:def 4;
then consider p being
Real such that A4:
p > 0
and A5:
Ball (
v,
p)
c= M
by A1, Def5;
v in N
by A3, XBOOLE_0:def 4;
then consider r being
Real such that A6:
r > 0
and A7:
Ball (
v,
r)
c= N
by A2, Def5;
take q =
min (
p,
r);
( q > 0 & Ball (v,q) c= M /\ N )
thus
q > 0
by A4, A6, XXREAL_0:15;
Ball (v,q) c= M /\ N
Ball (
v,
q)
c= Ball (
v,
r)
by Th33, XXREAL_0:17;
then A8:
Ball (
v,
q)
c= N
by A7;
Ball (
v,
q)
c= Ball (
v,
p)
by Th33, XXREAL_0:17;
then
Ball (
v,
q)
c= M
by A5;
hence
Ball (
v,
q)
c= M /\ N
by A8, XBOOLE_1:19;
verum
end;
hence
M /\ N in Family_open_set V
by Def5; verum