let p1 be Point of (TOP-REAL 2); :: thesis: for a, b, r being real number 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 number ; :: 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 EUCLID:33;
then (1 * p1) + (1 * p1) = ((2 * |[a,b]|) - p1) + p1 by EUCLID:33;
then (1 + 1) * p1 = ((2 * |[a,b]|) - p1) + p1 by EUCLID:37;
then 2 * p1 = (2 * |[a,b]|) - (p1 - p1) by EUCLID:51;
then 2 * p1 = (2 * |[a,b]|) - (0. (TOP-REAL 2)) by EUCLID:46;
then 2 * p1 = (2 * |[a,b]|) + (0. (TOP-REAL 2)) by RLVECT_1:25;
then 2 * p1 = 2 * |[a,b]| by EUCLID:31;
then p1 = |[a,b]| by EUCLID:38;
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 EUCLID:30
.= |.(((2 * |[a,b]|) + ((- 1) * |[a,b]|)) + (- p1)).| by EUCLID:43
.= |.(((2 + (- 1)) * |[a,b]|) + (- p1)).| by EUCLID:37
.= |.(|[a,b]| - p1).| by EUCLID:33
.= 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 EUCLID:36
.= (1 / 2) * ((p1 + (- p1)) + (2 * |[a,b]|)) by EUCLID:30
.= (1 / 2) * ((0. (TOP-REAL 2)) + (2 * |[a,b]|)) by EUCLID:40
.= (1 / 2) * (2 * |[a,b]|) by EUCLID:31
.= ((1 / 2) * 2) * |[a,b]| by EUCLID:34
.= |[a,b]| by EUCLID:33 ;
hence |[a,b]| in LSeg p1,((2 * |[a,b]|) - p1) ; :: thesis: verum