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

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
A11: {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, A9, A11, 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 A10; :: thesis: verum

end;

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

hence m = u by A8; :: 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
A12: {e} = (halfline (s,t)) /\ (Sphere (o,r)) by A1, A3, Th4;
m = e by A7, A12, TARSKI:def 1;
hence m = u by A9, A12, TARSKI:def 1; :: thesis: verum

end;

end;