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 ( 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)
then ( the carrier of (Tcircle o,r) = Sphere o,r & HC s,t,o,r in (halfline s,t) /\ (Sphere o,r) ) by Def3, TOPREALB:9;
hence HC s,t,o,r is Point of (Tcircle o,r) by XBOOLE_0:def 4; :: thesis: verum