defpred S₁[ Point of , set ] means $2 = HC $1,f;
A1: for x being Point of ex m being Point of st S₁[x,m] ;
ex h being Function of (Tdisk o,r),(Tcircle o,r) st
for x being Point of 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 holds b₁ . x = HC x,f ; :: thesis: verum