:: deftheorem Def4 defines HC BROUWER:def 4 :
for n being non zero Element of NAT
for o being Point of (TOP-REAL n)
for r being non negative Real
for x being Point of (Tdisk (o,r))
for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) st not x is_a_fixpoint_of f holds
for b₆ being Point of (Tcircle (o,r)) holds
( b₆ = HC (x,f) iff ex y, z being Point of (TOP-REAL n) st
( y = x & z = f . x & b₆ = HC (z,y,o,r) ) );