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