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