let r be real number ; :: 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 number such that
A1: ( 0 < g1 & ].(r - g1),(r + g1).[ = N1 ) by Def7;
consider g2 being real number such that
A2: ( 0 < g2 & ].(r - g2),(r + g2).[ = N2 ) by Def7;
set g = min g1,g2;
A3: 0 < min g1,g2 by A1, A2, XXREAL_0:15;
A4: ( min g1,g2 <= g2 & min g1,g2 <= g1 ) by XXREAL_0:17;
then A5: r + (min g1,g2) <= r + g2 by XREAL_1:9;
A6: r + (min g1,g2) <= r + g1 by A4, XREAL_1:9;
- g2 <= - (min g1,g2) by A4, XREAL_1:26;
then A7: r + (- g2) <= r + (- (min g1,g2)) by XREAL_1:9;
- g1 <= - (min g1,g2) by A4, XREAL_1:26;
then A8: r + (- g1) <= r + (- (min g1,g2)) by XREAL_1:9;

A9: now

per cases ( g1 <= g2 or g2 <= g1 ) ;

suppose g1 <= g2 ; :: thesis: ( ].(r - (min g1,g2)),(r + (min g1,g2)).[ c= N1 & ].(r - (min g1,g2)),(r + (min g1,g2)).[ c= N2 )

then A10: g1 = min g1,g2 by XXREAL_0:def 9;

now

let y be set ; :: thesis: ( y in ].(r - (min g1,g2)),(r + (min g1,g2)).[ implies y in ].(r - g2),(r + g2).[ )
assume A11: y in ].(r - (min g1,g2)),(r + (min g1,g2)).[ ; :: thesis: y in ].(r - g2),(r + g2).[
then A12: ex p2 being Real st
( y = p2 & r - (min g1,g2) < p2 & p2 < r + (min g1,g2) ) ;
reconsider x1 = y as Real by A11;
A13: x1 < r + g2 by A5, A12, XXREAL_0:2;
r - g2 < x1 by A7, A12, XXREAL_0:2;
hence y in ].(r - g2),(r + g2).[ by A13; :: thesis: verum

end;

hence ( ].(r - (min g1,g2)),(r + (min g1,g2)).[ c= N1 & ].(r - (min g1,g2)),(r + (min g1,g2)).[ c= N2 ) by A1, A2, A10, TARSKI:def 3; :: thesis: verum

end;

suppose g2 <= g1 ; :: thesis: ( ].(r - (min g1,g2)),(r + (min g1,g2)).[ c= N1 & ].(r - (min g1,g2)),(r + (min g1,g2)).[ c= N2 )

then A14: g2 = min g1,g2 by XXREAL_0:def 9;

now

let y be set ; :: thesis: ( y in ].(r - (min g1,g2)),(r + (min g1,g2)).[ implies y in ].(r - g1),(r + g1).[ )
assume A15: y in ].(r - (min g1,g2)),(r + (min g1,g2)).[ ; :: thesis: y in ].(r - g1),(r + g1).[
then A16: ex p2 being Real st
( y = p2 & r - (min g1,g2) < p2 & p2 < r + (min g1,g2) ) ;
reconsider x1 = y as Real by A15;
A17: x1 < r + g1 by A6, A16, XXREAL_0:2;
r - g1 < x1 by A8, A16, XXREAL_0:2;
hence y in ].(r - g1),(r + g1).[ by A17; :: thesis: verum

end;

hence ( ].(r - (min g1,g2)),(r + (min g1,g2)).[ c= N1 & ].(r - (min g1,g2)),(r + (min g1,g2)).[ c= N2 ) by A1, A2, A14, TARSKI:def 3; :: thesis: verum

end;

end;

end;

reconsider N = ].(r - (min g1,g2)),(r + (min g1,g2)).[ as Neighbourhood of r by A3, Def7;
take N ; :: thesis: ( N c= N1 & N c= N2 )
thus ( N c= N1 & N c= N2 ) by A9; :: thesis: verum