let r be real number ; 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 ; 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); ( y in Sphere x,r implies (LSeg x,y) \ {x,y} c= Ball x,r )
assume A1:
y in Sphere x,r
; (LSeg x,y) \ {x,y} c= Ball x,r
per cases
( r = 0 or r <> 0 )
;
suppose A2:
r = 0
;
(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;
verum end; suppose A6:
r <> 0
;
(LSeg x,y) \ {x,y} c= Ball x,rlet k be
set ;
TARSKI:def 3 ( not k in (LSeg x,y) \ {x,y} or k in Ball x,r )assume A7:
k in (LSeg x,y) \ {x,y}
;
k in Ball x,rthen
k in LSeg x,
y
by XBOOLE_0:def 5;
then consider l being
Real such that A8:
k = ((1 - l) * x) + (l * y)
and A9:
0 <= l
and A10:
l <= 1
;
reconsider k =
k as
Point of
(TOP-REAL n) by A8;
not
k in {x,y}
by A7, XBOOLE_0:def 5;
then
k <> y
by TARSKI:def 2;
then
l <> 1
by A8, TOPREAL9:4;
then A11:
l < 1
by A10, XXREAL_0:1;
k - x =
(((1 - l) * x) - x) + (l * y)
by A8, 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 A12:
|.(k - x).| =
(abs l) * |.(y - x).|
by TOPRNS_1:8
.=
l * |.(y - x).|
by A9, ABSVALUE:def 1
.=
l * r
by A1, TOPREAL9:9
;
0 <= r
by A1;
then
l * r < 1
* r
by A6, A11, XREAL_1:70;
hence
k in Ball x,
r
by A12, TOPREAL9:7;
verum end;