let m, u be Point of (); :: 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 ;
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 ;
hence m = u by ; :: thesis: verum
end;
end;