set D = Sphere ((0. (TOP-REAL 2)),p1);
let p be Point of (Tunit_circle 2); :: thesis: Topen_unit_circle p, I(01) are_homeomorphic
set P = Topen_unit_circle p;
reconsider p2 = p as Point of (TOP-REAL 2) by PRE_TOPC:25;
(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} as Subset of (Tcircle ((0. (TOP-REAL 2)),1)) by Th9;
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, I(01) are_homeomorphic by Lm13, BORSUK_4:52, EUCLID:54; :: thesis: verum