let r be real number ; :: thesis: for n being Element of NAT
for y, x being Point of (TOP-REAL n) st y in Sphere x,r holds
(LSeg x,y) \ {x,y} c= Ball x,r
let n be Element of NAT ; :: thesis: for y, x being Point of (TOP-REAL n) st y in Sphere x,r holds
(LSeg x,y) \ {x,y} c= Ball x,r
let y, x be Point of (TOP-REAL n); :: thesis: ( y in Sphere x,r implies (LSeg x,y) \ {x,y} c= Ball x,r )
assume A1:
y in Sphere x,r
; :: thesis: (LSeg x,y) \ {x,y} c= Ball x,r
per cases
( r = 0 or r <> 0 )
;
suppose A2:
r = 0
;
:: thesis: (LSeg x,y) \ {x,y} c= Ball x,rreconsider xe =
x as
Point of
(Euclid n) by TOPREAL3:13;
Sphere x,
r = Sphere xe,
r
by TOPREAL9:15;
then
Sphere x,
r = {x}
by A2, TOPREAL6:62;
then A3:
x = y
by A1, TARSKI:def 1;
A4:
LSeg x,
x = {x}
by RLTOPSP1:71;
A5:
{x,x} = {x}
by ENUMSET1:69;
{x} \ {x} = {}
by XBOOLE_1:37;
hence
(LSeg x,y) \ {x,y} c= Ball x,
r
by A3, A4, A5, XBOOLE_1:2;
:: thesis: verum end; suppose A6:
r <> 0
;
:: thesis: (LSeg x,y) \ {x,y} c= Ball x,rlet k be
set ;
:: according to TARSKI:def 3 :: thesis: ( not k in (LSeg x,y) \ {x,y} or k in Ball x,r )assume A7:
k in (LSeg x,y) \ {x,y}
;
:: thesis: k in Ball x,rthen
k in LSeg x,
y
by XBOOLE_0:def 5;
then consider l being
Real such that A9:
k = ((1 - l) * x) + (l * y)
and A8:
(
0 <= l &
l <= 1 )
;
reconsider k =
k as
Point of
(TOP-REAL n) by A9;
not
k in {x,y}
by A7, XBOOLE_0:def 5;
then
(
k <> x &
k <> y )
by TARSKI:def 2;
then
(
0 <> l &
l <> 1 )
by A9, TOPREAL9:4;
then A10:
(
0 < l &
l < 1 )
by A8, XXREAL_0:1;
k - x =
(((1 - l) * x) - x) + (l * y)
by A9, JORDAN2C:9
.=
(((1 * x) - (l * x)) - x) + (l * y)
by EUCLID:54
.=
((x - (l * x)) - x) + (l * y)
by EUCLID:33
.=
((x - x) - (l * x)) + (l * y)
by TOPREAL9:1
.=
((0. (TOP-REAL n)) - (l * x)) + (l * y)
by EUCLID:46
.=
(l * y) - (l * x)
by EUCLID:31
.=
l * (y - x)
by EUCLID:53
;
then A11:
|.(k - x).| =
(abs l) * |.(y - x).|
by TOPRNS_1:8
.=
l * |.(y - x).|
by A8, ABSVALUE:def 1
.=
l * r
by A1, TOPREAL9:9
;
0 <= r
by A1;
then
l * r < 1
* r
by A6, A10, XREAL_1:70;
hence
k in Ball x,
r
by A11, TOPREAL9:7;
:: thesis: verum end;