let n be non empty Element of NAT ; :: thesis: for o, p being Point of (TOP-REAL n)
for r being positive real number st p in Ball o,r holds
RotateCircle o,r,p has_no_fixpoint
let o, p be Point of (TOP-REAL n); :: thesis: for r being positive real number st p in Ball o,r holds
RotateCircle o,r,p has_no_fixpoint
let r be positive real number ; :: thesis: ( p in Ball o,r implies RotateCircle o,r,p has_no_fixpoint )
assume A1: p in Ball o,r ; :: thesis: RotateCircle o,r,p has_no_fixpoint
set f = RotateCircle o,r,p;
let x be set ; :: according to ABIAN:def 5 :: thesis: not x is_a_fixpoint_of RotateCircle o,r,p
assume A2: x in dom (RotateCircle o,r,p) ; :: according to ABIAN:def 3 :: thesis: not x = (RotateCircle o,r,p) . x
set S = Tcircle o,r;
A3: dom (RotateCircle o,r,p) = the carrier of (Tcircle o,r) by FUNCT_2:def 1;
consider y being Point of (TOP-REAL n) such that
A4: x = y and
A5: (RotateCircle o,r,p) . x = HC y,p,o,r by A1, A2, Def8;
A6: the carrier of (Tcircle o,r) = Sphere o,r by TOPREALB:9;
Sphere o,r c= cl_Ball o,r by TOPREAL9:17;
then A7: y is Point of (Tdisk o,r) by A2, A3, A4, A6, BROUWER:3;
Ball o,r c= cl_Ball o,r by TOPREAL9:16;
then A8: p is Point of (Tdisk o,r) by A1, BROUWER:3;
Ball o,r misses Sphere o,r by TOPREAL9:19;
then y <> p by A1, A2, A4, A6, XBOOLE_0:3;
hence not x = (RotateCircle o,r,p) . x by A4, A5, A7, A8, BROUWER:def 3; :: thesis: verum