per cases ( s is Point of or not s is Point of ) ;

suppose s is Point of ; :: thesis: ex b₁ being Point of st
( b₁ in (halfline s,t) /\ (Sphere o,r) & b₁ <> s )

then consider e being Point of such that
A4: ( e <> s & {s,e} = (halfline s,t) /\ (Sphere o,r) ) by A2, A3, Th5;
reconsider e = e as Point of by PRE_TOPC:55;
take e ; :: thesis: ( e in (halfline s,t) /\ (Sphere o,r) & e <> s )
thus ( e in (halfline s,t) /\ (Sphere o,r) & e <> s ) by A4, TARSKI:def 2; :: thesis: verum

end;

suppose A5: s is not Point of ; :: thesis: ex b₁ being Point of st
( b₁ in (halfline s,t) /\ (Sphere o,r) & b₁ <> s )

then consider e1 being Point of such that
A6: {e1} = (halfline s,t) /\ (Sphere o,r) by A1, A3, Th4;
reconsider e1 = e1 as Point of by PRE_TOPC:55;
take e1 ; :: thesis: ( e1 in (halfline s,t) /\ (Sphere o,r) & e1 <> s )
thus ( e1 in (halfline s,t) /\ (Sphere o,r) & e1 <> s ) by A5, A6, TARSKI:def 1; :: thesis: verum

end;

end;