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