let r, r1, s, s1 be Real; :: 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 Th21;
A2: |[((r1 + s1) / 2),s]| `1 = ((1 - (1 / 2)) * (|[r1,s]| `1)) + ((1 / 2) * (|[s1,s]| `1))
.= (((1 - (1 / 2)) * |[r1,s]|) `1) + ((1 / 2) * (|[s1,s]| `1)) by Th4
.= (((1 - (1 / 2)) * |[r1,s]|) `1) + (((1 / 2) * |[s1,s]|) `1) by Th4
.= (((1 - (1 / 2)) * |[r1,s]|) + ((1 / 2) * |[s1,s]|)) `1 by Th2 ;
|[((r1 + s1) / 2),s]| `2 = ((1 - (1 / 2)) * (|[r1,s]| `2)) + ((1 / 2) * (|[s1,s]| `2))
.= (((1 - (1 / 2)) * |[r1,s]|) `2) + ((1 / 2) * (|[s1,s]| `2)) by Th4
.= (((1 - (1 / 2)) * |[r1,s]|) `2) + (((1 / 2) * |[s1,s]|) `2) by Th4
.= (((1 - (1 / 2)) * |[r1,s]|) + ((1 / 2) * |[s1,s]|)) `2 by Th2 ;
then |[((r1 + s1) / 2),s]| = ((1 - (1 / 2)) * |[r1,s]|) + ((1 / 2) * |[s1,s]|) by A2, Th6;
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