let r be non negative real number ; :: thesis: for n being non empty Element of NAT
for s, o, t being Point of (TOP-REAL n) st s is Point of (Tdisk o,r) & t is Point of (Tdisk o,r) & s <> t holds
HC s,t,o,r is Point of (Tcircle o,r)
let n be non empty Element of NAT ; :: thesis: for s, o, t being Point of (TOP-REAL n) st s is Point of (Tdisk o,r) & t is Point of (Tdisk o,r) & s <> t holds
HC s,t,o,r is Point of (Tcircle o,r)
let s, o, t be Point of (TOP-REAL n); :: thesis: ( s is Point of (Tdisk o,r) & t is Point of (Tdisk o,r) & s <> t implies HC s,t,o,r is Point of (Tcircle o,r) )
assume A1: ( s is Point of (Tdisk o,r) & t is Point of (Tdisk o,r) & s <> t ) ; :: thesis: HC s,t,o,r is Point of (Tcircle o,r)
A2: the carrier of (Tcircle o,r) = Sphere o,r by TOPREALB:9;
HC s,t,o,r in (halfline s,t) /\ (Sphere o,r) by A1, Def3;
hence HC s,t,o,r is Point of (Tcircle o,r) by A2, XBOOLE_0:def 4; :: thesis: verum