A2: 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 );
A3: 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 A4: 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 A4, PRE_TOPC:55;
Sphere o,r c= cl_Ball o,r by TOPREAL9:17;
then A5: z is Point of (Tdisk o,r) by A2, A4, BROUWER:3;
Ball o,r c= cl_Ball o,r by TOPREAL9:16;
then A6: p is Point of (Tdisk o,r) by A1, BROUWER:3;
Ball o,r misses Sphere o,r by TOPREAL9:19;
then p <> z by A1, A2, A4, XBOOLE_0:3;
then HC z,p,o,r is Point of (Tcircle o,r) by A5, A6, 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
A7: for x being set st x in the carrier of (Tcircle o,r) holds
S₁[x,f . x] from FUNCT_2:sch 1(A3);
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 A7; :: thesis: verum