let r be Real; :: thesis: for N1, N2 being Neighbourhood of r ex N being Neighbourhood of r st
( N c= N1 & N c= N2 )
let N1, N2 be Neighbourhood of r; :: thesis: ex N being Neighbourhood of r st
( N c= N1 & N c= N2 )
consider g1 being Real such that
A1: 0 < g1 and
A2: ].(r - g1),(r + g1).[ = N1 by Def6;
consider g2 being Real such that
A3: 0 < g2 and
A4: ].(r - g2),(r + g2).[ = N2 by Def6;
set g = min (g1,g2);
0 < min (g1,g2) by A1, A3, XXREAL_0:15;
then reconsider N = ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ as Neighbourhood of r by Def6;
take N ; :: thesis: ( N c= N1 & N c= N2 )
A5: min (g1,g2) <= g1 by XXREAL_0:17;
then A6: r + (min (g1,g2)) <= r + g1 by XREAL_1:7;
- g1 <= - (min (g1,g2)) by A5, XREAL_1:24;
then A7: r + (- g1) <= r + (- (min (g1,g2))) by XREAL_1:7;
A8: min (g1,g2) <= g2 by XXREAL_0:17;
then - g2 <= - (min (g1,g2)) by XREAL_1:24;
then A9: r + (- g2) <= r + (- (min (g1,g2))) by XREAL_1:7;
A10: r + (min (g1,g2)) <= r + g2 by A8, XREAL_1:7;
now :: thesis: ( ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N1 & ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N2 )
per cases ( g1 <= g2 or g2 <= g1 ) ;
suppose A11: g1 <= g2 ; :: thesis: ( ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N1 & ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N2 )
A12: now :: thesis: for y being object st y in ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ holds
y in ].(r - g2),(r + g2).[
let y be object ; :: thesis: ( y in ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ implies y in ].(r - g2),(r + g2).[ )
assume A13: y in ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ ; :: thesis: y in ].(r - g2),(r + g2).[
then reconsider x1 = y as Real ;
ex p2 being Real st
( y = p2 & r - (min (g1,g2)) < p2 & p2 < r + (min (g1,g2)) ) by A13;
then ( x1 < r + g2 & r - g2 < x1 ) by A10, A9, XXREAL_0:2;
hence y in ].(r - g2),(r + g2).[ ; :: thesis: verum
end;
g1 = min (g1,g2) by A11, XXREAL_0:def 9;
hence ( ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N1 & ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N2 ) by A2, A4, A12; :: thesis: verum
end;
suppose A14: g2 <= g1 ; :: thesis: ( ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N1 & ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N2 )
A15: now :: thesis: for y being object st y in ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ holds
y in ].(r - g1),(r + g1).[
let y be object ; :: thesis: ( y in ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ implies y in ].(r - g1),(r + g1).[ )
assume A16: y in ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ ; :: thesis: y in ].(r - g1),(r + g1).[
then reconsider x1 = y as Real ;
ex p2 being Real st
( y = p2 & r - (min (g1,g2)) < p2 & p2 < r + (min (g1,g2)) ) by A16;
then ( x1 < r + g1 & r - g1 < x1 ) by A6, A7, XXREAL_0:2;
hence y in ].(r - g1),(r + g1).[ ; :: thesis: verum
end;
g2 = min (g1,g2) by A14, XXREAL_0:def 9;
hence ( ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N1 & ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N2 ) by A2, A4, A15; :: thesis: verum
end;
end;
end;
hence ( N c= N1 & N c= N2 ) ; :: thesis: verum