let m, u be Point of (TOP-REAL n); :: thesis: ( m in (halfline (s,t)) /\ (Sphere (o,r)) & m <> s & u in (halfline (s,t)) /\ (Sphere (o,r)) & u <> s implies m = u )

assume that

A7: m in (halfline (s,t)) /\ (Sphere (o,r)) and

A8: m <> s and

A9: u in (halfline (s,t)) /\ (Sphere (o,r)) and

A10: u <> s ; :: thesis: m = u

assume that

A7: m in (halfline (s,t)) /\ (Sphere (o,r)) and

A8: m <> s and

A9: u in (halfline (s,t)) /\ (Sphere (o,r)) and

A10: u <> s ; :: thesis: m = u

per cases
( s is Point of (Tcircle (o,r)) or not s is Point of (Tcircle (o,r)) )
;

end;

suppose
s is Point of (Tcircle (o,r))
; :: thesis: m = u

then consider f1 being Point of (Tcircle (o,r)) such that

f1 <> s and

A11: {s,f1} = (halfline (s,t)) /\ (Sphere (o,r)) by A2, A3, Th5;

end;f1 <> s and

A11: {s,f1} = (halfline (s,t)) /\ (Sphere (o,r)) by A2, A3, Th5;