let n be Nat; :: thesis: for r being Real
for y, z, x being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Sphere (x,r) holds
(halfline (y,z)) /\ (Sphere (x,r)) = {y,z}
let r be Real; :: thesis: for y, z, x being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Sphere (x,r) holds
(halfline (y,z)) /\ (Sphere (x,r)) = {y,z}
let y, z, x be Point of (TOP-REAL n); :: thesis: ( y in Sphere (x,r) & z in Sphere (x,r) implies (halfline (y,z)) /\ (Sphere (x,r)) = {y,z} )
assume that
A1: y in Sphere (x,r) and
A2: z in Sphere (x,r) ; :: thesis: (halfline (y,z)) /\ (Sphere (x,r)) = {y,z}

per cases ( y = z or y <> z ) ;

suppose A3: y = z ; :: thesis: (halfline (y,z)) /\ (Sphere (x,r)) = {y,z}

then A4: {y,z} = {y} by ENUMSET1:29;
A5: halfline (y,z) = {y} by A3, Th27;
hence for m being object st m in (halfline (y,z)) /\ (Sphere (x,r)) holds
m in {y,z} by A4, XBOOLE_0:def 4; :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {y,z} c= (halfline (y,z)) /\ (Sphere (x,r))
let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in {y,z} or m in (halfline (y,z)) /\ (Sphere (x,r)) )
assume A6: m in {y,z} ; :: thesis: m in (halfline (y,z)) /\ (Sphere (x,r))
then m = y by A4, TARSKI:def 1;
hence m in (halfline (y,z)) /\ (Sphere (x,r)) by A1, A5, A4, A6, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A7: y <> z ; :: thesis: (halfline (y,z)) /\ (Sphere (x,r)) = {y,z}

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

let m be object ; :: thesis: ( m in (halfline (y,z)) /\ (Sphere (x,r)) implies b₁ in {y,z} )
assume A8: m in (halfline (y,z)) /\ (Sphere (x,r)) ; :: thesis: b₁ in {y,z}
then A9: m in Sphere (x,r) by XBOOLE_0:def 4;
reconsider w = m as Point of (TOP-REAL n) by A8;
m in halfline (y,z) by A8, XBOOLE_0:def 4;
then consider R being Real such that
A10: m = ((1 - R) * y) + (R * z) and
A11: 0 <= R ;
reconsider R = R as Real ;

per cases ( R = 0 or R = 1 or ( R > 0 & R < 1 ) or R > 1 ) by A11, XXREAL_0:1;

suppose R = 0 ; :: thesis: b₁ in {y,z}

then m = y by A10, Th2;
hence m in {y,z} by TARSKI:def 2; :: thesis: verum

end;

suppose R = 1 ; :: thesis: b₁ in {y,z}

then m = z by A10, Th2;
hence m in {y,z} by TARSKI:def 2; :: thesis: verum

end;

suppose A12: ( R > 0 & R < 1 ) ; :: thesis: b₁ in {y,z}

A13: now :: thesis: not m in {y,z}

assume m in {y,z} ; :: thesis: contradiction
then ( m = y or m = z ) by TARSKI:def 2;
hence contradiction by A7, A10, A12, Th2; :: thesis: verum

end;

w in LSeg (y,z) by A10, A12;
then A14: m in (LSeg (y,z)) \ {y,z} by A13, XBOOLE_0:def 5;
(LSeg (y,z)) \ {y,z} c= Ball (x,r) by A1, A2, Th32;
then |.(w - x).| < r by A14, Th5;
hence m in {y,z} by A9, Th7; :: thesis: verum

end;

suppose A15: R > 1 ; :: thesis: b₁ in {y,z}

then A16: 1 / R < 1 by XREAL_1:212;
A17: ((1 - (1 / R)) * y) + ((1 / R) * w) = ((1 - (1 / R)) * y) + (((1 / R) * ((1 - R) * y)) + ((1 / R) * (R * z))) by A10, RLVECT_1:def 5
.= ((1 - (1 / R)) * y) + (((1 / R) * ((1 - R) * y)) + (((1 / R) * R) * z)) by RLVECT_1:def 7
.= ((1 - (1 / R)) * y) + (((1 / R) * ((1 - R) * y)) + (1 * z)) by A15, XCMPLX_1:87
.= ((1 - (1 / R)) * y) + (((1 / R) * ((1 - R) * y)) + z) by RLVECT_1:def 8
.= (((1 - (1 / R)) * y) + ((1 / R) * ((1 - R) * y))) + z by RLVECT_1:def 3
.= (((1 - (1 / R)) * y) + (((1 / R) * (1 - R)) * y)) + z by RLVECT_1:def 7
.= (((1 - (1 / R)) + ((1 / R) * (1 - R))) * y) + z by RLVECT_1:def 6
.= ((((1 - (1 / R)) + ((1 / R) * 1)) - ((1 / R) * R)) * y) + z
.= ((((1 - (1 / R)) + ((1 / R) * 1)) - 1) * y) + z by A15, XCMPLX_1:87
.= (0. (TOP-REAL n)) + z by RLVECT_1:10
.= z by RLVECT_1:4 ;

A18: now :: thesis: not z in {y,w}

assume z in {y,w} ; :: thesis: contradiction
then ( z = y or z = w ) by TARSKI:def 2;
hence contradiction by A7, A16, A17, Th2; :: thesis: verum

end;

z in LSeg (y,w) by A15, A16, A17;
then A19: z in (LSeg (y,w)) \ {y,w} by A18, XBOOLE_0:def 5;
(LSeg (y,w)) \ {y,w} c= Ball (x,r) by A1, A9, Th32;
then |.(z - x).| < r by A19, Th5;
hence m in {y,z} by A2, Th7; :: thesis: verum

end;

end;

end;

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in {y,z} or m in (halfline (y,z)) /\ (Sphere (x,r)) )
assume m in {y,z} ; :: thesis: m in (halfline (y,z)) /\ (Sphere (x,r))
then A20: ( m = y or m = z ) by TARSKI:def 2;
( y in halfline (y,z) & z in halfline (y,z) ) by Th25, Th26;
hence m in (halfline (y,z)) /\ (Sphere (x,r)) by A1, A2, A20, XBOOLE_0:def 4; :: thesis: verum

end;

end;