A1: the carrier of (Tcircle (o,r)) = Sphere (o,r) by TOPREALB:9;
defpred S₁[ set , set ] means ex z being Point of (TOP-REAL n) st
( $1 = z & $2 = HC (z,p,o,r) );
A2: for x being set st x in the carrier of (Tcircle (o,r)) holds
ex y being set st
( y in the carrier of (Tcircle (o,r)) & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in the carrier of (Tcircle (o,r)) implies ex y being set st
( y in the carrier of (Tcircle (o,r)) & S₁[x,y] ) )
assume A3: x in the carrier of (Tcircle (o,r)) ; :: thesis: ex y being set st
( y in the carrier of (Tcircle (o,r)) & S₁[x,y] )
reconsider z = x as Point of (TOP-REAL n) by A3, PRE_TOPC:25;
Sphere (o,r) c= cl_Ball (o,r) by TOPREAL9:17;
then A4: z is Point of (Tdisk (o,r)) by A1, A3, BROUWER:3;
Ball (o,r) c= cl_Ball (o,r) by TOPREAL9:16;
then A5: p is Point of (Tdisk (o,r)) by B1, BROUWER:3;
Ball (o,r) misses Sphere (o,r) by TOPREAL9:19;
then p <> z by B1, A1, A3, XBOOLE_0:3;
then HC (z,p,o,r) is Point of (Tcircle (o,r)) by A4, A5, BROUWER:6;
hence ex y being set st
( y in the carrier of (Tcircle (o,r)) & S₁[x,y] ) ; :: thesis: verum

end;

consider f being Function of the carrier of (Tcircle (o,r)), the carrier of (Tcircle (o,r)) such that
A6: for x being set st x in the carrier of (Tcircle (o,r)) holds
S₁[x,f . x] from FUNCT_2:sch 1(A2);
reconsider f = f as Function of (Tcircle (o,r)),(Tcircle (o,r)) ;
take f ; :: thesis: for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st
( x = y & f . x = HC (y,p,o,r) )
let x be Point of (Tcircle (o,r)); :: thesis: ex y being Point of (TOP-REAL n) st
( x = y & f . x = HC (y,p,o,r) )
thus ex y being Point of (TOP-REAL n) st
( x = y & f . x = HC (y,p,o,r) ) by A6; :: thesis: verum