set T = Tcircle ((0. (TOP-REAL 2)),r);
set C = [#] (Tcircle ((0. (TOP-REAL 2)),r));
[#] (Tcircle ((0. (TOP-REAL 2)),r)) c= [#] (TOP-REAL 2)
by PRE_TOPC:def 4;
then reconsider C = [#] (Tcircle ((0. (TOP-REAL 2)),r)) as Subset of (TOP-REAL 2) ;
A1:
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;
then reconsider f = Rotate s as Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) ;
A2:
( f is onto & f is isometric )
by JORDAN24:2;
reconsider A = C as Subset of (TopSpaceMetr (Euclid 2)) by A1;
(TOP-REAL 2) | C = Tcircle ((0. (TOP-REAL 2)),r)
by PRE_TOPC:def 5;
then A3:
(TopSpaceMetr (Euclid 2)) | A = Tcircle ((0. (TOP-REAL 2)),r)
by A1, PRE_TOPC:36;
the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) = Sphere ((0. (TOP-REAL 2)),r)
by TOPREALB:9;
then
(Rotate s) .: C = C
by Th49;
hence
RotateCircle (r,s) is being_homeomorphism
by A2, A3, JORDAN24:14; verum