let n be non zero Nat; :: thesis: 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); :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: according to BORSUK_7:def 11 :: thesis: ( 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; :: thesis: 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; :: thesis: verum