set D = Sphere (0. (TOP-REAL 2)),p1;
let p, q be Point of (Tunit_circle 2); :: thesis: 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; :: thesis: verum