let V be RealUnitarySpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( v in M /\ N implies ex q being Real st
( q > 0 & Ball (v,q) c= M /\ N ) )
assume A3: v in M /\ N ; :: thesis: 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); :: thesis: ( q > 0 & Ball (v,q) c= M /\ N )
thus q > 0 by A4, A6, XXREAL_0:15; :: thesis: 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; :: thesis: verum

end;

hence M /\ N in Family_open_set V by Def5; :: thesis: verum