let p be Point of (TUnitSphere n); :: thesis: ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic
reconsider n1 = n + 1 as Element of NAT by ORDINAL1:def 12;
[#] (Tunit_circle (n + 1)) c= [#] (TOP-REAL (n + 1)) by PRE_TOPC:def 4;
then reconsider p1 = p as Point of (TOP-REAL n1) ;
A1: |.p1.| = 1 by TOPREALB:12;
A2: |.(- p1).| = sqrt |((- p1),(- p1))| by EUCLID_2:37
.= sqrt |(p1,p1)| by EUCLID_2:23
.= 1 by A1, EUCLID_2:37 ;
then |.((- p1) + (0. (TOP-REAL n1))).| = 1 by RLVECT_1:4;
then |.((- p1) + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by RLVECT_1:10;
then B3: |.((- p1) - (0. (TOP-REAL n1))).| = 1 by RLVECT_1:16;
then - p1 in Sphere ((0. (TOP-REAL n1)),1) by TOPREAL9:9;
then - p1 in [#] ((TOP-REAL n1) | (Sphere ((0. (TOP-REAL n1)),1))) by PRE_TOPC:def 5;
then - p1 in the carrier of (Tcircle ((0. (TOP-REAL n1)),1)) by TOPREALB:def 6;
then - p1 in the carrier of (Tunit_circle n1) by TOPREALB:def 7;
then reconsider A = {(- p1)} as Subset of (TUnitSphere n) by ZFMISC_1:31;
reconsider U1 = ([#] (TUnitSphere n)) \ A as Subset of (TUnitSphere n) ;
|.(0. (TOP-REAL n1)).| <> |.(- p1).| by A2, EUCLID_2:39;
then 0. (TOP-REAL n1) <> (1 + 1) * (- p1) by RLVECT_1:11;
then 0. (TOP-REAL n1) <> (1 * (- p1)) + (1 * (- p1)) by RLVECT_1:def 6;
then 0. (TOP-REAL n1) <> (1 * (- p1)) + (- p1) by RLVECT_1:def 8;
then 0. (TOP-REAL n1) <> (- p1) + (- p1) by RLVECT_1:def 8;
then (- p1) + (- (- p1)) <> (- p1) + (- p1) by RLVECT_1:5;
then A4: not p1 in {(- p1)} by TARSKI:def 1;
then p1 in U1 by XBOOLE_0:def 5;
then reconsider U = U1 as a_neighborhood of p by CONNSP_2:3, FRECHET:4;
take U ; :: thesis: U, [#] (TOP-REAL n) are_homeomorphic
reconsider m = n + 1 as Nat ;
A5: TUnitSphere n = Tcircle ((0. (TOP-REAL m)),1) by TOPREALB:def 7
.= (TOP-REAL m) | (Sphere ((0. (TOP-REAL m)),1)) by TOPREALB:def 6 ;
reconsider S = Sphere ((0. (TOP-REAL m)),1) as Subset of (TOP-REAL m) ;
reconsider U11 = U1 as Subset of ((TOP-REAL m) | S) by A5;
U1 c= [#] (Tunit_circle m) ;
then A6: U1 c= Sphere ((0. (TOP-REAL m)),1) by A5, PRE_TOPC:def 5;
then reconsider V = U11 as non empty Subset of (TOP-REAL m) by A4, XBOOLE_0:def 5, XBOOLE_1:1;
(TUnitSphere n) | U = (TOP-REAL m) | V by A5, A6, PRE_TOPC:7;
then reconsider U2 = (TUnitSphere n) | U as non empty SubSpace of TOP-REAL m ;
reconsider p2 = - p1 as Point of (TOP-REAL m) ;
p2 <> 0. (TOP-REAL m) by A2, EUCLID_2:39;
then A7: TOP-REAL n, TPlane (p2,(0. (TOP-REAL m))) are_homeomorphic by Th29;
A8: (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93;
A9: TOP-REAL n, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by YELLOW14:19;
[#] U2 = U by PRE_TOPC:def 5
.= the carrier of (Tcircle ((0. (TOP-REAL m)),1)) \ {p2} by TOPREALB:def 7
.= ([#] ((TOP-REAL m) | (Sphere ((0. (TOP-REAL m)),1)))) \ {p2} by TOPREALB:def 6
.= (Sphere ((0. (TOP-REAL m)),1)) \ {p2} by PRE_TOPC:def 5 ;
then stereographic_projection (U2,p2) is being_homeomorphism by B3, TOPREAL9:9, Th31;
then U2, TPlane (p2,(0. (TOP-REAL m))) are_homeomorphic by T_0TOPSP:def 1;
then TOP-REAL n,U2 are_homeomorphic by A7, BORSUK_3:3;
hence U, [#] (TOP-REAL n) are_homeomorphic by A8, METRIZTS:def 1, A9, BORSUK_3:3; :: thesis: verum