let p be Point of (Tdisk ((0. (TOP-REAL n)),1)); :: according to MFOLD_0:def 3 :: thesis: ex U being a_neighborhood of p st (Tdisk ((0. (TOP-REAL n)),1)) | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic
Int ([#] (Tdisk ((0. (TOP-REAL n)),1))) = [#] (Tdisk ((0. (TOP-REAL n)),1)) by TOPS_1:15;
then reconsider CM = [#] (Tdisk ((0. (TOP-REAL n)),1)) as non empty a_neighborhood of p by CONNSP_2:def 1;
take CM ; :: thesis: (Tdisk ((0. (TOP-REAL n)),1)) | CM, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic
thus (Tdisk ((0. (TOP-REAL n)),1)) | CM, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by TSEP_1:93; :: thesis: verum