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, XBOOLE_1:1;
Ball v,q c= Ball v,p by Th33, XXREAL_0:17;
then Ball v,q c= M by A5, XBOOLE_1:1;
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