A1: for x being set holds
( x in Int M iff ex U being Subset of M st
( U is open & U c= Int M & x in U ) ) set p = the Point of M;
consider U being a_neighborhood of the Point of M, n being Nat such that
A5: M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by Def2;
A6: [#] (M | U) = U by PRE_TOPC:def 5;
then reconsider IU = Int U as Subset of (M | U) by TOPS_1:16;
set MU = M | U;
set TR = TOP-REAL n;
consider h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) such that
A7: h is being_homeomorphism by T_0TOPSP:def 1, A5;
IU is open by TSEP_1:9;
then h .: IU is open by A7, TOPGRP_1:25;
then h .: IU in the topology of (Tdisk ((0. (TOP-REAL n)),1)) by PRE_TOPC:def 2;
then consider W being Subset of (TOP-REAL n) such that
A8: W in the topology of (TOP-REAL n) and
A9: h .: IU = W /\ ([#] (Tdisk ((0. (TOP-REAL n)),1))) by PRE_TOPC:def 4;
A10: [#] (Tdisk ((0. (TOP-REAL n)),1)) = cl_Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;
A11: dom h = [#] (M | U) by A7, TOPS_2:def 5;
A12: Ball ((0. (TOP-REAL n)),1) c= cl_Ball ((0. (TOP-REAL n)),1) by TOPREAL9:16;
reconsider W = W as open Subset of (TOP-REAL n) by A8, PRE_TOPC:def 2;
set WB = W /\ (Ball ((0. (TOP-REAL n)),1));
the Point of M in Int U by CONNSP_2:def 1;
then A13: h . the Point of M in h .: IU by A11, FUNCT_1:def 6;
then A14: h . the Point of M in W by A9, XBOOLE_0:def 4;
then reconsider hp = h . the Point of M as Point of (TOP-REAL n) ;
A15: h .: IU = W /\ (cl_Ball ((0. (TOP-REAL n)),1)) by PRE_TOPC:def 5, A9;
not W /\ (Ball ((0. (TOP-REAL n)),1)) is empty then consider wb being set such that
A30: wb in W /\ (Ball ((0. (TOP-REAL n)),1)) ;
reconsider wb = wb as Point of (TOP-REAL n) by A30;
reconsider wbE = wb as Point of (Euclid n) by EUCLID:67;
Int (W /\ (Ball ((0. (TOP-REAL n)),1))) = W /\ (Ball ((0. (TOP-REAL n)),1)) by TOPS_1:23;
then consider s being Real such that
A31: s > 0 and
A32: Ball (wbE,s) c= W /\ (Ball ((0. (TOP-REAL n)),1)) by A30, GOBOARD6:5;
A33: Ball (wb,s) = Ball (wbE,s) by TOPREAL9:13;
W /\ (Ball ((0. (TOP-REAL n)),1)) c= Ball ((0. (TOP-REAL n)),1) by XBOOLE_1:17;
then A34: Ball (wb,s) c= Ball ((0. (TOP-REAL n)),1) by A32, A33;
then reconsider BB = Ball (wb,s) as Subset of (Tdisk ((0. (TOP-REAL n)),1)) by A12, XBOOLE_1:1, A10;
A35: (Tdisk ((0. (TOP-REAL n)),1)) | BB = (TOP-REAL n) | (Ball (wb,s)) by A34, A12, XBOOLE_1:1, PRE_TOPC:7;
reconsider hBB = h " BB as Subset of M by A6, XBOOLE_1:1;
BB is open by TSEP_1:9;
then A36: h " BB is open by A7, TOPGRP_1:26;
W /\ (Ball ((0. (TOP-REAL n)),1)) c= h .: IU by A10, A9, TOPREAL9:16, XBOOLE_1:26;
then BB c= h .: IU by A32, A33;
then A37: h " BB c= h " (h .: IU) by RELAT_1:143;
h " (h .: IU) c= IU by FUNCT_1:82, A7;
then h " BB c= IU by A37;
then hBB is open by A36, TSEP_1:9;
then A38: Int hBB = hBB by TOPS_1:23;
A39: rng h = [#] (Tdisk ((0. (TOP-REAL n)),1)) by A7, TOPS_2:def 5;
then A40: h .: (h " BB) = BB by FUNCT_1:77;
not hBB is empty by A31, RELAT_1:139, A39;
then consider t being set such that
A41: t in hBB ;
reconsider t = t as Point of M by A41;
reconsider hBB = hBB as a_neighborhood of t by A38, CONNSP_2:def 1, A41;
A43: (M | U) | (h " BB) = M | hBB by A6, PRE_TOPC:7;
then reconsider HH = h | (h " BB) as Function of (M | hBB),((TOP-REAL n) | (Ball (wb,s))) by A40, A35, JORDAN24:12;
HH is being_homeomorphism by A7, A40, A35, A43, METRIZTS:2;
then A44: M | hBB,(TOP-REAL n) | (Ball (wb,s)) are_homeomorphic by T_0TOPSP:def 1;
Tball (wb,s), Tball ((0. (TOP-REAL n)),1) are_homeomorphic by Th3, A31;
then M | hBB, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A44, A31, BORSUK_3:3;
hence ( not Int M is empty & Int M is open ) by A1, TOPS_1:25, Def4; :: thesis: verum