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

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