let S be RealNormSpace; :: thesis: for x being Point of S
for N1, N2 being Neighbourhood of x holds N1 /\ N2 is Neighbourhood of x
let x be Point of S; :: thesis: for N1, N2 being Neighbourhood of x holds N1 /\ N2 is Neighbourhood of x
let N1, N2 be Neighbourhood of x; :: thesis: N1 /\ N2 is Neighbourhood of x
consider N being Neighbourhood of x such that
A1: ( N c= N1 & N c= N2 ) by NDIFF_1:1;
A2: N c= N1 /\ N2 by A1, XBOOLE_1:19;
consider g being Real such that
A3: 0 < g and
A4: { y where y is Point of S : ||.(y - x).|| < g } c= N by NFCONT_1:def 1;
{ y where y is Point of S : ||.(y - x).|| < g } c= N1 /\ N2 by A2, A4;
hence N1 /\ N2 is Neighbourhood of x by A3, NFCONT_1:def 1; :: thesis: verum