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