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) & m <> s ) and
A8: ( u in (halfline s,t) /\ (Sphere o,r) & u <> s ) ; :: thesis: m = u

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

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
A9: {s,f1} = (halfline s,t) /\ (Sphere o,r) by A2, A3, Th5;

per cases ( ( m = f1 & u = f1 ) or ( m = f1 & u = s ) or ( m = s & u = f1 ) or ( m = s & u = s ) ) by A7, A8, A9, TARSKI:def 2;

suppose ( m = f1 & u = f1 ) ; :: thesis: m = u

hence m = u ; :: thesis: verum

end;

suppose ( m = f1 & u = s ) ; :: thesis: m = u

hence m = u by A8; :: thesis: verum

end;

suppose ( m = s & u = f1 ) ; :: thesis: m = u

hence m = u by A7; :: thesis: verum

end;

suppose ( m = s & u = s ) ; :: thesis: m = u

hence m = u ; :: thesis: verum

end;

end;

end;

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

then consider e being Point of (Tcircle o,r) such that
A10: {e} = (halfline s,t) /\ (Sphere o,r) by A1, A3, Th4;
m = e by A7, A10, TARSKI:def 1;
hence m = u by A8, A10, TARSKI:def 1; :: thesis: verum

end;

end;