let r be Real; 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; 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
; ( 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 ( ].(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
;
( ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N1 & ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N2 )A12:
now 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 ;
( 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))).[
;
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).[
;
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;
verum end; suppose A14:
g2 <= g1
;
( ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N1 & ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N2 )A15:
now 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 ;
( 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))).[
;
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).[
;
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;
verum end; end; end;
hence
( N c= N1 & N c= N2 )
; verum