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 1;

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 1;

set g = min (g1,g2);

take { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } ; :: thesis: ( { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } is Element of K16( the carrier of S) & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } is Neighbourhood of x0 & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } c= N1 & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } 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 }

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

hence ( { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } is Element of K16( the carrier of S) & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } is Neighbourhood of x0 & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } c= N1 & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } c= N2 ) by A2, A4, A10, A6, NFCONT_1:3; :: thesis: verum

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 1;

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 1;

set g = min (g1,g2);

take { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } ; :: thesis: ( { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } is Element of K16( the carrier of S) & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } is Neighbourhood of x0 & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } c= N1 & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } 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

A9:
min (g1,g2) <= g1
by XXREAL_0:17;
let z be object ; :: 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;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

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

0 < min (g1,g2)
by A1, A3, XXREAL_0:15;
let z be object ; :: 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;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

hence ( { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } is Element of K16( the carrier of S) & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } is Neighbourhood of x0 & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } c= N1 & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } c= N2 ) by A2, A4, A10, A6, NFCONT_1:3; :: thesis: verum