let n be non empty Nat; :: thesis: for p, x, y, x1, y1 being Point of (TOP-REAL n)
for r being real positive number 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 real positive number 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 real positive number ; :: 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, Def12;
hence x1 is Point of (Tcircle (p,r)) by A2, FUNCT_2:5; :: according to BORSUK_7:def 12 :: 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, Def12;
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, Def12;
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, Def6
.= ((1 - a) * (r * x)) + ((1 - a) * p) by EUCLID:32
.= ((r * (1 - a)) * x) + ((1 - a) * p) by EUCLID:30
.= (r * ((1 - a) * x)) + ((1 - a) * p) by EUCLID:30 ;
a * y1 = a * ((r * y) + p) by A3, A5, Def6
.= (a * (r * y)) + (a * p) by EUCLID:32
.= ((r * a) * y) + (a * p) by EUCLID:30
.= (r * (a * y)) + (a * p) by EUCLID:30 ;
then ((1 - a) * x1) + (a * y1) = (((r * ((1 - a) * x)) + ((1 - a) * p)) + (r * (a * y))) + (a * p) by A8, EUCLID:26
.= (((r * ((1 - a) * x)) + (r * (a * y))) + ((1 - a) * p)) + (a * p) by EUCLID:26
.= ((r * (((1 - a) * x) + (a * y))) + ((1 - a) * p)) + (a * p) by EUCLID:32
.= ((0. (TOP-REAL n)) + ((1 - a) * p)) + (a * p) by A6, EUCLID:28
.= ((1 - a) * p) + (a * p) by EUCLID:27
.= ((1 * p) - (a * p)) + (a * p) by EUCLID:50
.= 1 * p by EUCLID:48
.= p by EUCLID:29 ;
hence p in LSeg (x1,y1) by A7; :: thesis: verum