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) by Th28;
( |[r1,s]| `1 = r1 & |[s1,s]| `1 = s1 ) by EUCLID:52;
then A2: |[((r1 + s1) / 2),s]| `1 = ((1 - (1 / 2)) * (|[r1,s]| `1)) + ((1 / 2) * (|[s1,s]| `1)) by EUCLID:52
.= (((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 ;
( |[r1,s]| `2 = s & |[s1,s]| `2 = s ) by EUCLID:52;
then |[((r1 + s1) / 2),s]| `2 = ((1 - (1 / 2)) * (|[r1,s]| `2)) + ((1 / 2) * (|[s1,s]| `2)) by EUCLID:52
.= (((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 ;
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