let r be non negative real number ; :: thesis: for n being non empty Element of NAT
for s, o, t being Point of st s is Point of & t is Point of & s <> t holds
HC s,t,o,r is Point of
let n be non empty Element of NAT ; :: thesis: for s, o, t being Point of st s is Point of & t is Point of & s <> t holds
HC s,t,o,r is Point of
let s, o, t be Point of ; :: thesis: ( s is Point of & t is Point of & s <> t implies HC s,t,o,r is Point of )
assume ( s is Point of & t is Point of & s <> t ) ; :: thesis: HC s,t,o,r is Point of
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 by XBOOLE_0:def 4; :: thesis: verum