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: ex b₁ being Point of (TOP-REAL n) st
( b₁ in (halfline (s,t)) /\ (Sphere (o,r)) & b₁ <> s )

then consider e being Point of (Tcircle (o,r)) such that
A4: ( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (o,r)) ) by A2, A3, Th5;
reconsider e = e as Point of (TOP-REAL n) by PRE_TOPC:25;
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 (Tcircle (o,r)) ; :: thesis: ex b₁ being Point of (TOP-REAL n) st
( b₁ in (halfline (s,t)) /\ (Sphere (o,r)) & b₁ <> s )

then consider e1 being Point of (Tcircle (o,r)) such that
A6: {e1} = (halfline (s,t)) /\ (Sphere (o,r)) by A1, A3, Th4;
reconsider e1 = e1 as Point of (TOP-REAL n) by PRE_TOPC:25;
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;