defpred S₁[ Point of (Tdisk (o,r)), set ] means $2 = HC ($1,f);
A1: for x being Point of (Tdisk (o,r)) ex m being Point of (Tcircle (o,r)) st S₁[x,m] ;
ex h being Function of (Tdisk (o,r)),(Tcircle (o,r)) st
for x being Point of (Tdisk (o,r)) holds S₁[x,h . x] from FUNCT_2:sch 3(A1);
hence ex b₁ being Function of (Tdisk (o,r)),(Tcircle (o,r)) st
for x being Point of (Tdisk (o,r)) holds b₁ . x = HC (x,f) ; :: thesis: verum