let n be Element of NAT ; :: thesis: for r being real number
for y, x, z being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Ball (x,r) holds
(LSeg (y,z)) /\ (Sphere (x,r)) = {y}
let r be real number ; :: thesis: for y, x, z being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Ball (x,r) holds
(LSeg (y,z)) /\ (Sphere (x,r)) = {y}
let y, x, z be Point of (TOP-REAL n); :: thesis: ( y in Sphere (x,r) & z in Ball (x,r) implies (LSeg (y,z)) /\ (Sphere (x,r)) = {y} )
set s = y;
set t = z;
assume that
A1: y in Sphere (x,r) and
A2: z in Ball (x,r) ; :: thesis: (LSeg (y,z)) /\ (Sphere (x,r)) = {y}

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {y} c= (LSeg (y,z)) /\ (Sphere (x,r))

let m be set ; :: thesis: ( m in (LSeg (y,z)) /\ (Sphere (x,r)) implies b₁ in {y} )
assume A3: m in (LSeg (y,z)) /\ (Sphere (x,r)) ; :: thesis: b₁ in {y}
then reconsider w = m as Point of (TOP-REAL n) ;
w in LSeg (y,z) by A3, XBOOLE_0:def 4;
then consider d being Real such that
A4: 0 <= d and
A5: d <= 1 and
A6: w = ((1 - d) * y) + (d * z) by JGRAPH_1:35;
A7: |.(d * (z - x)).| = (abs d) * |.(z - x).| by TOPRNS_1:7
.= d * |.(z - x).| by A4, ABSVALUE:def 1 ;
d - 1 <= 1 - 1 by A5, XREAL_1:9;
then A8: - 0 <= - (d - 1) ;
A9: |.((1 - d) * (y - x)).| = (abs (1 - d)) * |.(y - x).| by TOPRNS_1:7
.= (1 - d) * |.(y - x).| by A8, ABSVALUE:def 1
.= (1 - d) * r by A1, Th9 ;
m in Sphere (x,r) by A3, XBOOLE_0:def 4;
then A10: r = |.(w - x).| by Th9
.= |.((((1 - d) * y) + (d * z)) - (((1 - d) + d) * x)).| by A6, EUCLID:29
.= |.((((1 - d) * y) + (d * z)) - (((1 - d) * x) + (d * x))).| by EUCLID:33
.= |.(((((1 - d) * y) + (d * z)) - ((1 - d) * x)) - (d * x)).| by EUCLID:46
.= |.(((((1 - d) * y) - ((1 - d) * x)) + (d * z)) - (d * x)).| by JORDAN2C:7
.= |.((((1 - d) * (y - x)) + (d * z)) - (d * x)).| by EUCLID:49
.= |.(((1 - d) * (y - x)) + ((d * z) - (d * x))).| by EUCLID:45
.= |.(((1 - d) * (y - x)) + (d * (z - x))).| by EUCLID:49 ;

per cases ( d > 0 or d = 0 ) by A4;

suppose A11: d > 0 ; :: thesis: b₁ in {y}

|.(z - x).| < r by A2, Th7;
then d * |.(z - x).| < d * r by A11, XREAL_1:68;
then ((1 - d) * r) + (d * |.(z - x).|) < ((1 - d) * r) + (d * r) by XREAL_1:8;
hence m in {y} by A10, A9, A7, TOPRNS_1:29; :: thesis: verum

end;

suppose d = 0 ; :: thesis: b₁ in {y}

then m = (1 * y) + (0. (TOP-REAL n)) by A6, EUCLID:29
.= 1 * y by EUCLID:27
.= y by EUCLID:29 ;
hence m in {y} by TARSKI:def 1; :: thesis: verum

end;

end;

end;

let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in {y} or m in (LSeg (y,z)) /\ (Sphere (x,r)) )
A12: y in LSeg (y,z) by RLTOPSP1:68;
assume m in {y} ; :: thesis: m in (LSeg (y,z)) /\ (Sphere (x,r))
then m = y by TARSKI:def 1;
hence m in (LSeg (y,z)) /\ (Sphere (x,r)) by A1, A12, XBOOLE_0:def 4; :: thesis: verum