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 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 A1: ( s in circle (a,b,r) & 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:8;
A2: inside_of_circle (a,b,r) = Ball (e,r) by Th46
.= Ball (|[a,b]|,r) by Th11 ;
circle (a,b,r) = Sphere (e,r) by Th47
.= Sphere (|[a,b]|,r) by Th13 ;
hence (LSeg (s,t)) /\ (circle (a,b,r)) = {s} by A1, A2, Th31; :: thesis: verum