let S be RealNormSpace; :: thesis: for x0 being Point of S
for N1, N2 being Neighbourhood of x0 ex N being Neighbourhood of x0 st
( N c= N1 & N c= N2 )
let x0 be Point of S; :: thesis: for N1, N2 being Neighbourhood of x0 ex N being Neighbourhood of x0 st
( N c= N1 & N c= N2 )
let N1, N2 be Neighbourhood of x0; :: thesis: ex N being Neighbourhood of x0 st
( N c= N1 & N c= N2 )
consider g1 being Real such that
A1: 0 < g1 and
A2: { y where y is Point of S : ||.(y - x0).|| < g1 } c= N1 by NFCONT_1:def 3;
consider g2 being Real such that
A3: 0 < g2 and
A4: { y where y is Point of S : ||.(y - x0).|| < g2 } c= N2 by NFCONT_1:def 3;
set g = min g1,g2;
take N = { y where y is Point of S : ||.(y - x0).|| < min g1,g2 } ; :: thesis: ( N is Element of K21(the carrier of S) & N is Neighbourhood of x0 & N c= N1 & N c= N2 )
A5: min g1,g2 <= g2 by XXREAL_0:17;
A6: { y where y is Point of S : ||.(y - x0).|| < min g1,g2 } c= { y where y is Point of S : ||.(y - x0).|| < g2 }

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { y where y is Point of S : ||.(y - x0).|| < min g1,g2 } or z in { y where y is Point of S : ||.(y - x0).|| < g2 } )
assume z in { y where y is Point of S : ||.(y - x0).|| < min g1,g2 } ; :: thesis: z in { y where y is Point of S : ||.(y - x0).|| < g2 }
then consider y being Point of S such that
A7: z = y and
A8: ||.(y - x0).|| < min g1,g2 ;
||.(y - x0).|| < g2 by A5, A8, XXREAL_0:2;
hence z in { y where y is Point of S : ||.(y - x0).|| < g2 } by A7; :: thesis: verum

end;

A9: min g1,g2 <= g1 by XXREAL_0:17;
A10: { y where y is Point of S : ||.(y - x0).|| < min g1,g2 } c= { y where y is Point of S : ||.(y - x0).|| < g1 }

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { y where y is Point of S : ||.(y - x0).|| < min g1,g2 } or z in { y where y is Point of S : ||.(y - x0).|| < g1 } )
assume z in { y where y is Point of S : ||.(y - x0).|| < min g1,g2 } ; :: thesis: z in { y where y is Point of S : ||.(y - x0).|| < g1 }
then consider y being Point of S such that
A11: z = y and
A12: ||.(y - x0).|| < min g1,g2 ;
||.(y - x0).|| < g1 by A9, A12, XXREAL_0:2;
hence z in { y where y is Point of S : ||.(y - x0).|| < g1 } by A11; :: thesis: verum

end;

0 < min g1,g2 by A1, A3, XXREAL_0:15;
hence ( N is Element of K21(the carrier of S) & N is Neighbourhood of x0 & N c= N1 & N c= N2 ) by A2, A4, A10, A6, NFCONT_1:3, XBOOLE_1:1; :: thesis: verum