A2:
the carrier of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) = (cl_Ball (o,r)) \ {p}
by PRE_TOPC:8;
defpred S1[ object , object ] means ex z being Point of (TOP-REAL n) st
( $1 = z & $2 = HC (p,z,o,r) );
A3:
for x being object st x in the carrier of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) holds
ex y being object st
( y in the carrier of (Tcircle (o,r)) & S1[x,y] )
proof
let x be
object ;
( x in the carrier of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) implies ex y being object st
( y in the carrier of (Tcircle (o,r)) & S1[x,y] ) )
assume A4:
x in the
carrier of
((TOP-REAL n) | ((cl_Ball (o,r)) \ {p}))
;
ex y being object st
( y in the carrier of (Tcircle (o,r)) & S1[x,y] )
reconsider z =
x as
Point of
(TOP-REAL n) by A4, PRE_TOPC:25;
z in cl_Ball (
o,
r)
by A2, A4, XBOOLE_0:def 5;
then A5:
z is
Point of
(Tdisk (o,r))
by BROUWER:3;
p <> z
by A2, A4, ZFMISC_1:56;
then
HC (
p,
z,
o,
r) is
Point of
(Tcircle (o,r))
by A1, A5, BROUWER:6;
hence
ex
y being
object st
(
y in the
carrier of
(Tcircle (o,r)) &
S1[
x,
y] )
;
verum
end;
consider f being Function of the carrier of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})), the carrier of (Tcircle (o,r)) such that
A6:
for x being object st x in the carrier of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) holds
S1[x,f . x]
from FUNCT_2:sch 1(A3);
reconsider f = f as Function of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})),(Tcircle (o,r)) ;
take
f
; for x being Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex y being Point of (TOP-REAL n) st
( x = y & f . x = HC (p,y,o,r) )
let x be Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})); ex y being Point of (TOP-REAL n) st
( x = y & f . x = HC (p,y,o,r) )
thus
ex y being Point of (TOP-REAL n) st
( x = y & f . x = HC (p,y,o,r) )
by A6; verum