for n being 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