let s, r1, r, s1 be real number ; :: thesis: for u being Point of (Euclid 2) st |[s,r1]| in Ball u,r & |[s,s1]| in Ball u,r holds
|[s,((r1 + s1) / 2)]| in Ball u,r
let u be Point of (Euclid 2); :: thesis: ( |[s,r1]| in Ball u,r & |[s,s1]| in Ball u,r implies |[s,((r1 + s1) / 2)]| in Ball u,r )
set p = |[s,r1]|;
set q = |[s,s1]|;
set p3 = |[s,((r1 + s1) / 2)]|;
assume ( |[s,r1]| in Ball u,r & |[s,s1]| in Ball u,r ) ; :: thesis: |[s,((r1 + s1) / 2)]| in Ball u,r
then A1: ( LSeg |[s,r1]|,|[s,s1]| c= Ball u,r & |[s,r1]| `1 = s & |[s,r1]| `2 = r1 & |[s,s1]| `1 = s & |[s,s1]| `2 = s1 & 2 <> 0 ) by Th28, EUCLID:56;
then A2: |[s,((r1 + s1) / 2)]| `1 = ((1 - (1 / 2)) * (|[s,r1]| `1 )) + ((1 / 2) * (|[s,s1]| `1 )) by EUCLID:56
.= (((1 - (1 / 2)) * |[s,r1]|) `1 ) + ((1 / 2) * (|[s,s1]| `1 )) by Th9
.= (((1 - (1 / 2)) * |[s,r1]|) `1 ) + (((1 / 2) * |[s,s1]|) `1 ) by Th9
.= (((1 - (1 / 2)) * |[s,r1]|) + ((1 / 2) * |[s,s1]|)) `1 by Th7 ;
|[s,((r1 + s1) / 2)]| `2 = ((1 - (1 / 2)) * (|[s,r1]| `2 )) + ((1 / 2) * (|[s,s1]| `2 )) by A1, EUCLID:56
.= (((1 - (1 / 2)) * |[s,r1]|) `2 ) + ((1 / 2) * (|[s,s1]| `2 )) by Th9
.= (((1 - (1 / 2)) * |[s,r1]|) `2 ) + (((1 / 2) * |[s,s1]|) `2 ) by Th9
.= (((1 - (1 / 2)) * |[s,r1]|) + ((1 / 2) * |[s,s1]|)) `2 by Th7 ;
then |[s,((r1 + s1) / 2)]| = ((1 - (1 / 2)) * |[s,r1]|) + ((1 / 2) * |[s,s1]|) by A2, Th11;
then |[s,((r1 + s1) / 2)]| in { (((1 - lambda) * |[s,r1]|) + (lambda * |[s,s1]|)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } ;
hence |[s,((r1 + s1) / 2)]| in Ball u,r by A1; :: thesis: verum