let r be non negative Real; :: thesis: for n being non zero Element of NAT
for s, t, o 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 zero Element of NAT ; :: thesis: for s, t, o 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, t, o 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