let n be non zero Nat; for p, x, y, x1, y1 being Point of (TOP-REAL n)
for r being positive Real st x,y are_antipodals_of 0. (TOP-REAL n),1 & x1 = (CircleIso (p,r)) . x & y1 = (CircleIso (p,r)) . y holds
x1,y1 are_antipodals_of p,r
let p, x, y, x1, y1 be Point of (TOP-REAL n); for r being positive Real st x,y are_antipodals_of 0. (TOP-REAL n),1 & x1 = (CircleIso (p,r)) . x & y1 = (CircleIso (p,r)) . y holds
x1,y1 are_antipodals_of p,r
let r be positive Real; ( x,y are_antipodals_of 0. (TOP-REAL n),1 & x1 = (CircleIso (p,r)) . x & y1 = (CircleIso (p,r)) . y implies x1,y1 are_antipodals_of p,r )
set h = CircleIso (p,r);
assume that
A1:
x,y are_antipodals_of 0. (TOP-REAL n),1
and
A2:
x1 = (CircleIso (p,r)) . x
and
A3:
y1 = (CircleIso (p,r)) . y
; x1,y1 are_antipodals_of p,r
A4:
x is Point of (Tcircle ((0. (TOP-REAL n)),1))
by A1;
hence
x1 is Point of (Tcircle (p,r))
by A2, FUNCT_2:5; BORSUK_7:def 11 ( y1 is Point of (Tcircle (p,r)) & p in LSeg (x1,y1) )
A5:
y is Point of (Tcircle ((0. (TOP-REAL n)),1))
by A1;
hence
y1 is Point of (Tcircle (p,r))
by A3, FUNCT_2:5; p in LSeg (x1,y1)
0. (TOP-REAL n) in LSeg (x,y)
by A1;
then consider a being Real such that
A6:
0. (TOP-REAL n) = ((1 - a) * x) + (a * y)
and
A7:
( 0 <= a & a <= 1 )
;
A8: (1 - a) * x1 =
(1 - a) * ((r * x) + p)
by A2, A4, Def5
.=
((1 - a) * (r * x)) + ((1 - a) * p)
by RLVECT_1:def 5
.=
((r * (1 - a)) * x) + ((1 - a) * p)
by RLVECT_1:def 7
.=
(r * ((1 - a) * x)) + ((1 - a) * p)
by RLVECT_1:def 7
;
a * y1 =
a * ((r * y) + p)
by A3, A5, Def5
.=
(a * (r * y)) + (a * p)
by RLVECT_1:def 5
.=
((r * a) * y) + (a * p)
by RLVECT_1:def 7
.=
(r * (a * y)) + (a * p)
by RLVECT_1:def 7
;
then ((1 - a) * x1) + (a * y1) =
(((r * ((1 - a) * x)) + ((1 - a) * p)) + (r * (a * y))) + (a * p)
by A8, RLVECT_1:def 3
.=
(((r * ((1 - a) * x)) + (r * (a * y))) + ((1 - a) * p)) + (a * p)
by RLVECT_1:def 3
.=
((r * (((1 - a) * x) + (a * y))) + ((1 - a) * p)) + (a * p)
by RLVECT_1:def 5
.=
((0. (TOP-REAL n)) + ((1 - a) * p)) + (a * p)
by A6, RLVECT_1:10
.=
((1 - a) * p) + (a * p)
by RLVECT_1:4
.=
((1 * p) - (a * p)) + (a * p)
by RLVECT_1:35
.=
1 * p
by RLVECT_4:1
.=
p
by RLVECT_1:def 8
;
hence
p in LSeg (x1,y1)
by A7; verum