let a, b, r be real number ; :: thesis: for s, t being Point of (TOP-REAL 2) st s in circle a,b,r & t in inside_of_circle a,b,r holds
(LSeg s,t) /\ (circle a,b,r) = {s}
let s, t be Point of (TOP-REAL 2); :: thesis: ( s in circle a,b,r & t in inside_of_circle a,b,r implies (LSeg s,t) /\ (circle a,b,r) = {s} )
assume that
A1: s in circle a,b,r and
A2: t in inside_of_circle a,b,r ; :: thesis: (LSeg s,t) /\ (circle a,b,r) = {s}
reconsider e = |[a,b]| as Point of (Euclid 2) by TOPREAL3:13;
A3: circle a,b,r = Sphere e,r by Th49
.= Sphere |[a,b]|,r by Th15 ;
inside_of_circle a,b,r = Ball e,r by Th48
.= Ball |[a,b]|,r by Th13 ;
hence (LSeg s,t) /\ (circle a,b,r) = {s} by A1, A2, A3, Th33; :: thesis: verum