set D = Sphere ((0. (TOP-REAL 2)),p1);
let p, q be Point of (Tunit_circle 2); Topen_unit_circle p, Topen_unit_circle q are_homeomorphic
set P = Topen_unit_circle p;
set Q = Topen_unit_circle q;
reconsider p2 = p, q2 = q as Point of (TOP-REAL 2) by PRE_TOPC:55;
A1:
(Sphere ((0. (TOP-REAL 2)),p1)) \ {q} c= Sphere ((0. (TOP-REAL 2)),p1)
by XBOOLE_1:36;
(Sphere ((0. (TOP-REAL 2)),p1)) \ {p} c= Sphere ((0. (TOP-REAL 2)),p1)
by XBOOLE_1:36;
then reconsider A = (Sphere ((0. (TOP-REAL 2)),p1)) \ {p}, B = (Sphere ((0. (TOP-REAL 2)),p1)) \ {q} as Subset of (Tcircle ((0. (TOP-REAL 2)),1)) by A1, Th9;
A2: Topen_unit_circle q =
(Tcircle ((0. (TOP-REAL 2)),1)) | B
by Lm13, Th23, EUCLID:58
.=
(TOP-REAL 2) | ((Sphere ((0. (TOP-REAL 2)),p1)) \ {q2})
by GOBOARD9:4
;
Topen_unit_circle p =
(Tcircle ((0. (TOP-REAL 2)),1)) | A
by Lm13, Th23, EUCLID:58
.=
(TOP-REAL 2) | ((Sphere ((0. (TOP-REAL 2)),p1)) \ {p2})
by GOBOARD9:4
;
hence
Topen_unit_circle p, Topen_unit_circle q are_homeomorphic
by A2, Lm13, BORSUK_4:78, EUCLID:58; verum