let a, b, r be Real; :: thesis: for s, t being Point of (TOP-REAL 2) st s in circle (a,b,r) & t in circle (a,b,r) holds
(LSeg (s,t)) \ {s,t} c= inside_of_circle (a,b,r)
let s, t be Point of (TOP-REAL 2); :: thesis: ( s in circle (a,b,r) & t in circle (a,b,r) implies (LSeg (s,t)) \ {s,t} c= inside_of_circle (a,b,r) )
assume A1: ( s in circle (a,b,r) & t in circle (a,b,r) ) ; :: thesis: (LSeg (s,t)) \ {s,t} c= inside_of_circle (a,b,r)
reconsider G = |[a,b]| as Point of (Euclid 2) by TOPREAL3:8;
Sphere (G,r) = circle (a,b,r) by Th47;
then A2: Sphere (|[a,b]|,r) = circle (a,b,r) by Th13;
Ball (|[a,b]|,r) = inside_of_circle (a,b,r) by Th48;
hence (LSeg (s,t)) \ {s,t} c= inside_of_circle (a,b,r) by A1, A2, Th32; :: thesis: verum