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

end;

suppose
s is Point of (Tcircle (o,r))
; :: thesis: ex b_{1} being Point of (TOP-REAL n) st

( b_{1} in (halfline (s,t)) /\ (Sphere (o,r)) & b_{1} <> s )

( b

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;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

suppose A5:
s is not Point of (Tcircle (o,r))
; :: thesis: ex b_{1} being Point of (TOP-REAL n) st

( b_{1} in (halfline (s,t)) /\ (Sphere (o,r)) & b_{1} <> s )

( b

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;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