let p1 be Point of (TOP-REAL 2); :: thesis: for a, b, r being Real st p1 in circle (a,b,r) & r > 0 holds
ex p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p2 in circle (a,b,r) & |[a,b]| in LSeg (p1,p2) )
let a, b, r be Real; :: thesis: ( p1 in circle (a,b,r) & r > 0 implies ex p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p2 in circle (a,b,r) & |[a,b]| in LSeg (p1,p2) ) )
set pc = |[a,b]|;
set p2 = (2 * |[a,b]|) - p1;
assume A1: p1 in circle (a,b,r) ; :: thesis: ( not r > 0 or ex p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p2 in circle (a,b,r) & |[a,b]| in LSeg (p1,p2) ) )
then A2: |.(p1 - |[a,b]|).| = r by TOPREAL9:43;
assume A3: r > 0 ; :: thesis: ex p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p2 in circle (a,b,r) & |[a,b]| in LSeg (p1,p2) )
take (2 * |[a,b]|) - p1 ; :: thesis: ( p1 <> (2 * |[a,b]|) - p1 & (2 * |[a,b]|) - p1 in circle (a,b,r) & |[a,b]| in LSeg (p1,((2 * |[a,b]|) - p1)) )
thus p1 <> (2 * |[a,b]|) - p1 :: thesis: ( (2 * |[a,b]|) - p1 in circle (a,b,r) & |[a,b]| in LSeg (p1,((2 * |[a,b]|) - p1)) )

proof

assume p1 = (2 * |[a,b]|) - p1 ; :: thesis: contradiction
then (1 * p1) + p1 = ((2 * |[a,b]|) - p1) + p1 by RLVECT_1:def 8;
then (1 * p1) + (1 * p1) = ((2 * |[a,b]|) - p1) + p1 by RLVECT_1:def 8;
then (1 + 1) * p1 = ((2 * |[a,b]|) - p1) + p1 by RLVECT_1:def 6;
then 2 * p1 = (2 * |[a,b]|) - (p1 - p1) by RLVECT_1:29;
then 2 * p1 = (2 * |[a,b]|) - (0. (TOP-REAL 2)) by RLVECT_1:5;
then 2 * p1 = (2 * |[a,b]|) + (0. (TOP-REAL 2)) by RLVECT_1:12;
then 2 * p1 = 2 * |[a,b]| by RLVECT_1:4;
then p1 = |[a,b]| by RLVECT_1:36;
then |.(|[a,b]| - |[a,b]|).| = r by A1, TOPREAL9:43;
hence contradiction by A3, Lm1; :: thesis: verum

end;

|.(((2 * |[a,b]|) - p1) - |[a,b]|).| = |.(((2 * |[a,b]|) - p1) - |[a,b]|).|
.= |.(((2 * |[a,b]|) + (- p1)) - |[a,b]|).|
.= |.(((2 * |[a,b]|) + (- |[a,b]|)) + (- p1)).| by RLVECT_1:def 3
.= |.(((2 * |[a,b]|) + ((- 1) * |[a,b]|)) + (- p1)).|
.= |.(((2 + (- 1)) * |[a,b]|) + (- p1)).| by RLVECT_1:def 6
.= |.(|[a,b]| - p1).| by RLVECT_1:def 8
.= r by A2, Lm2 ;
hence (2 * |[a,b]|) - p1 in circle (a,b,r) by TOPREAL9:43; :: thesis: |[a,b]| in LSeg (p1,((2 * |[a,b]|) - p1))
((1 - (1 / 2)) * p1) + ((1 / 2) * ((2 * |[a,b]|) - p1)) = (1 / 2) * (p1 + ((2 * |[a,b]|) - p1)) by RLVECT_1:def 5
.= (1 / 2) * ((p1 + (- p1)) + (2 * |[a,b]|)) by RLVECT_1:def 3
.= (1 / 2) * ((0. (TOP-REAL 2)) + (2 * |[a,b]|)) by RLVECT_1:5
.= (1 / 2) * (2 * |[a,b]|) by RLVECT_1:4
.= ((1 / 2) * 2) * |[a,b]| by RLVECT_1:def 7
.= |[a,b]| by RLVECT_1:def 8 ;
hence |[a,b]| in LSeg (p1,((2 * |[a,b]|) - p1)) ; :: thesis: verum