let n be non zero Element of NAT ; :: thesis: for o, p being Point of (TOP-REAL n)
for r being positive Real st p in Ball (o,r) holds
RotateCircle (o,r,p) is without_fixpoints
let o, p be Point of (TOP-REAL n); :: thesis: for r being positive Real st p in Ball (o,r) holds
RotateCircle (o,r,p) is without_fixpoints
let r be positive Real; :: thesis: ( p in Ball (o,r) implies RotateCircle (o,r,p) is without_fixpoints )
assume A1: p in Ball (o,r) ; :: thesis: RotateCircle (o,r,p) is without_fixpoints
set f = RotateCircle (o,r,p);
let x be object ; :: 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