let a, b, r be Real; :: thesis: for P, Q, R being Element of (TOP-REAL 2) st Q in LSeg (P,R) & P in inside_of_circle (a,b,r) & R in inside_of_circle (a,b,r) holds
Q in inside_of_circle (a,b,r)
let P, Q, R be Element of (TOP-REAL 2); :: thesis: ( Q in LSeg (P,R) & P in inside_of_circle (a,b,r) & R in inside_of_circle (a,b,r) implies Q in inside_of_circle (a,b,r) )
assume that
A1: Q in LSeg (P,R) and
A2: P in inside_of_circle (a,b,r) and
A3: R in inside_of_circle (a,b,r) ; :: thesis: Q in inside_of_circle (a,b,r)
consider s being Real such that
A4: ( 0 <= s & s <= 1 ) and
A5: Q = ((1 - s) * P) + (s * R) by A1, RLTOPSP1:76;
s in [.0,1.] by A4, XXREAL_1:1;
then ( s in ].0,1.[ or s = 0 or s = 1 ) by XXREAL_1:5;

per cases then ( ( 0 < s & s < 1 ) or s = 0 or s = 1 ) by XXREAL_1:4;

suppose A6: ( 0 < s & s < 1 ) ; :: thesis: Q in inside_of_circle (a,b,r)

Q = (s * R) + ((1 - s) * P) by A5;
hence Q in inside_of_circle (a,b,r) by A2, A3, A6, CONVEX1:def 2; :: thesis: verum

end;

suppose s = 0 ; :: thesis: Q in inside_of_circle (a,b,r)

then Q = P + (0 * R) by A5, RVSUM_1:52
.= P by GTARSKI2:2 ;
hence Q in inside_of_circle (a,b,r) by A2; :: thesis: verum

end;

suppose s = 1 ; :: thesis: Q in inside_of_circle (a,b,r)

then Q = R + (0 * P) by A5, RVSUM_1:52
.= R by GTARSKI2:2 ;
hence Q in inside_of_circle (a,b,r) by A3; :: thesis: verum

end;

end;