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