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:25;

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, Th22, EUCLID:54

.= (TOP-REAL 2) | ((Sphere ((0. (TOP-REAL 2)),p1)) \ {q2}) by GOBOARD9:2 ;

Topen_unit_circle p = (Tcircle ((0. (TOP-REAL 2)),1)) | A by Lm13, Th22, EUCLID:54

.= (TOP-REAL 2) | ((Sphere ((0. (TOP-REAL 2)),p1)) \ {p2}) by GOBOARD9:2 ;

hence Topen_unit_circle p, Topen_unit_circle q are_homeomorphic by A2, Lm13, BORSUK_4:53, EUCLID:54; :: thesis: verum

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:25;

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, Th22, EUCLID:54

.= (TOP-REAL 2) | ((Sphere ((0. (TOP-REAL 2)),p1)) \ {q2}) by GOBOARD9:2 ;

Topen_unit_circle p = (Tcircle ((0. (TOP-REAL 2)),1)) | A by Lm13, Th22, EUCLID:54

.= (TOP-REAL 2) | ((Sphere ((0. (TOP-REAL 2)),p1)) \ {p2}) by GOBOARD9:2 ;

hence Topen_unit_circle p, Topen_unit_circle q are_homeomorphic by A2, Lm13, BORSUK_4:53, EUCLID:54; :: thesis: verum