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

end;

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