let E be RealNormSpace; :: thesis: for r being Real
for z, y1, y2 being Point of E st y1 in cl_Ball (z,r) & y2 in cl_Ball (z,r) holds
[.y1,y2.] c= cl_Ball (z,r)
let r be Real; :: thesis: for z, y1, y2 being Point of E st y1 in cl_Ball (z,r) & y2 in cl_Ball (z,r) holds
[.y1,y2.] c= cl_Ball (z,r)
let z, y1, y2 be Point of E; :: thesis: ( y1 in cl_Ball (z,r) & y2 in cl_Ball (z,r) implies [.y1,y2.] c= cl_Ball (z,r) )
assume A1: ( y1 in cl_Ball (z,r) & y2 in cl_Ball (z,r) ) ; :: thesis: [.y1,y2.] c= cl_Ball (z,r)
then A2: ex y1q being Element of E st
( y1 = y1q & ||.(z - y1q).|| <= r ) ;
A3: ex y2q being Element of E st
( y2 = y2q & ||.(z - y2q).|| <= r ) by A1;
A4: [.y1,y2.] = { (((1 - r) * y1) + (r * y2)) where r is Real : ( 0 <= r & r <= 1 ) } by RLTOPSP1:def 2;
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in [.y1,y2.] or s in cl_Ball (z,r) )
assume s in [.y1,y2.] ; :: thesis: s in cl_Ball (z,r)
then consider p being Real such that
A5: ( s = ((1 - p) * y1) + (p * y2) & 0 <= p & p <= 1 ) by A4;
reconsider w = s as Point of E by A5;
((1 - p) * z) + (p * z) = ((1 - p) + p) * z by RLVECT_1:def 6
.= z by RLVECT_1:def 8 ;
then z - w = ((((1 - p) * z) + (p * z)) - ((1 - p) * y1)) - (p * y2) by A5, RLVECT_1:27
.= ((((1 - p) * z) + (- ((1 - p) * y1))) + (p * z)) - (p * y2) by RLVECT_1:def 3
.= (((1 - p) * z) - ((1 - p) * y1)) + ((p * z) + (- (p * y2))) by RLVECT_1:def 3
.= ((1 - p) * (z - y1)) + ((p * z) - (p * y2)) by RLVECT_1:34
.= ((1 - p) * (z - y1)) + (p * (z - y2)) by RLVECT_1:34 ;
then ||.(z - w).|| <= ||.((1 - p) * (z - y1)).|| + ||.(p * (z - y2)).|| by NORMSP_1:def 1;
then ||.(z - w).|| <= (|.(1 - p).| * ||.(z - y1).||) + ||.(p * (z - y2)).|| by NORMSP_1:def 1;
then A7: ||.(z - w).|| <= (|.(1 - p).| * ||.(z - y1).||) + (|.p.| * ||.(z - y2).||) by NORMSP_1:def 1;
A8: ( |.(1 - p).| = 1 - p & |.p.| = p ) by A5, COMPLEX1:43, XREAL_1:48;
0 <= 1 - p by A5, XREAL_1:48;
then A9: (1 - p) * ||.(z - y1).|| <= (1 - p) * r by A2, XREAL_1:64;
p * ||.(z - y2).|| <= p * r by A3, A5, XREAL_1:64;
then ((1 - p) * ||.(z - y1).||) + (p * ||.(z - y2).||) <= ((1 - p) * r) + (p * r) by A9, XREAL_1:7;
then ||.(z - w).|| <= ((1 - p) * r) + (p * r) by A7, A8, XXREAL_0:2;
hence s in cl_Ball (z,r) ; :: thesis: verum