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 ) )

proof

let x be set ; :: thesis: ( x in Int M iff ex U being Subset of M st
( U is open & U c= Int M & x in U ) )

hereby :: thesis: ( ex U being Subset of M st
( U is open & U c= Int M & x in U ) implies x in Int M )

assume A2: x in Int M ; :: thesis: ex W being Element of bool the carrier of M st
( W is open & W c= Int M & x in W )
then reconsider p = x as Point of M ;
consider U being a_neighborhood of p, n being Nat such that
A3: M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A2, Def3;
take W = Int U; :: thesis: ( W is open & W c= Int M & x in W )
W c= Int M

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in W or y in Int M )
assume A4: y in W ; :: thesis: y in Int M
then reconsider q = y as Point of M ;
U is a_neighborhood of q by A4, CONNSP_2:def 1;
hence y in Int M by Def3, A3; :: thesis: verum

end;

hence ( W is open & W c= Int M & x in W ) by CONNSP_2:def 1; :: thesis: verum

end;

thus ( ex U being Subset of M st
( U is open & U c= Int M & x in U ) implies x in Int M ) ; :: thesis: verum

end;

set p = the Point of M;
consider U being a_neighborhood of the Point of M, n being Nat such that
A7: M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by Def1;
A8: [#] (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
A9: h is being_homeomorphism by T_0TOPSP:def 1, A7;
IU is open by TSEP_1:9;
then h .: IU is open by A9, 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
A10: W in the topology of (TOP-REAL n) and
A11: h .: IU = W /\ ([#] (Tdisk ((0. (TOP-REAL n)),1))) by PRE_TOPC:def 4;
A12: [#] (Tdisk ((0. (TOP-REAL n)),1)) = cl_Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;
A13: dom h = [#] (M | U) by A9, TOPS_2:def 5;
A15: 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 A10, 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 A16: h . the Point of M in h .: IU by A13, FUNCT_1:def 6;
then A17: h . the Point of M in W by A11, XBOOLE_0:def 4;
then reconsider hp = h . the Point of M as Point of (TOP-REAL n) ;
A18: h .: IU = W /\ (cl_Ball ((0. (TOP-REAL n)),1)) by PRE_TOPC:def 5, A11;
not W /\ (Ball ((0. (TOP-REAL n)),1)) is empty

proof

reconsider HP = hp as Point of (Euclid n) by EUCLID:67;
A19: Ball ((0. (TOP-REAL n)),1) misses Sphere ((0. (TOP-REAL n)),1) by TOPREAL9:19;
A20: cl_Ball ((0. (TOP-REAL n)),1) = (Ball ((0. (TOP-REAL n)),1)) \/ (Sphere ((0. (TOP-REAL n)),1)) by TOPREAL9:18;
assume A21: W /\ (Ball ((0. (TOP-REAL n)),1)) is empty ; :: thesis: contradiction
then W /\ (cl_Ball ((0. (TOP-REAL n)),1)) = (W /\ (cl_Ball ((0. (TOP-REAL n)),1))) \ (W /\ (Ball ((0. (TOP-REAL n)),1)))
.= ((W /\ (cl_Ball ((0. (TOP-REAL n)),1))) \ W) \/ ((W /\ (cl_Ball ((0. (TOP-REAL n)),1))) \ (Ball ((0. (TOP-REAL n)),1))) by XBOOLE_1:54
.= {} \/ ((W /\ (cl_Ball ((0. (TOP-REAL n)),1))) \ (Ball ((0. (TOP-REAL n)),1))) by XBOOLE_1:17, XBOOLE_1:37
.= W /\ ((cl_Ball ((0. (TOP-REAL n)),1)) \ (Ball ((0. (TOP-REAL n)),1))) by XBOOLE_1:49
.= W /\ (Sphere ((0. (TOP-REAL n)),1)) by A19, A20, XBOOLE_1:88 ;
then hp in Sphere ((0. (TOP-REAL n)),1) by A18, A16, XBOOLE_0:def 4;
then A22: |.hp.| = 1 by TOPREAL9:12;
Int W = W by TOPS_1:23;
then consider s being Real such that
A23: s > 0 and
A24: Ball (HP,s) c= W by A17, GOBOARD6:5;
set s2 = s / 2;
set m = min ((s / 2),(1 / 2));
A25: min ((s / 2),(1 / 2)) <= s / 2 by XXREAL_0:17;
s / 2 < s by A23, XREAL_1:216;
then A26: min ((s / 2),(1 / 2)) < s by A25, XXREAL_0:2;
A27: Ball (HP,s) = Ball (hp,s) by TOPREAL9:13;
A28: min ((s / 2),(1 / 2)) > 0 by A23, XXREAL_0:21;
then A29: 1 - (min ((s / 2),(1 / 2))) < 1 - 0 by XREAL_1:6;
A30: |.(- (min ((s / 2),(1 / 2)))).| = - (- (min ((s / 2),(1 / 2)))) by A28, ABSVALUE:def 1;
A31: ((1 - (min ((s / 2),(1 / 2)))) * hp) - (0. (TOP-REAL n)) = (1 - (min ((s / 2),(1 / 2)))) * hp by RLVECT_1:13;
((1 - (min ((s / 2),(1 / 2)))) * hp) - hp = ((1 - (min ((s / 2),(1 / 2)))) * hp) - (1 * hp) by RLVECT_1:def 8
.= ((1 - (min ((s / 2),(1 / 2)))) - 1) * hp by RLVECT_1:35
.= (- (min ((s / 2),(1 / 2)))) * hp ;
then |.(((1 - (min ((s / 2),(1 / 2)))) * hp) - hp).| = |.(- (min ((s / 2),(1 / 2)))).| * 1 by A22, EUCLID:11;
then A32: (1 - (min ((s / 2),(1 / 2)))) * hp in Ball (hp,s) by A30, A26;
1 - (min ((s / 2),(1 / 2))) >= 1 - (1 / 2) by XXREAL_0:17, XREAL_1:10;
then |.(1 - (min ((s / 2),(1 / 2)))).| = 1 - (min ((s / 2),(1 / 2))) by ABSVALUE:def 1;
then |.((1 - (min ((s / 2),(1 / 2)))) * hp).| = (1 - (min ((s / 2),(1 / 2)))) * 1 by A22, EUCLID:11;
then (1 - (min ((s / 2),(1 / 2)))) * hp in Ball ((0. (TOP-REAL n)),1) by A31, A29;
hence contradiction by A32, A24, A27, A21, XBOOLE_0:def 4; :: thesis: verum

end;

then consider wb being set such that
A33: wb in W /\ (Ball ((0. (TOP-REAL n)),1)) ;
reconsider wb = wb as Point of (TOP-REAL n) by A33;
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
A34: s > 0 and
A35: Ball (wbE,s) c= W /\ (Ball ((0. (TOP-REAL n)),1)) by A33, GOBOARD6:5;
A36: 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 A37: Ball (wb,s) c= Ball ((0. (TOP-REAL n)),1) by A35, A36;
then reconsider BB = Ball (wb,s) as Subset of (Tdisk ((0. (TOP-REAL n)),1)) by A15, XBOOLE_1:1, A12;
A38: (Tdisk ((0. (TOP-REAL n)),1)) | BB = (TOP-REAL n) | (Ball (wb,s)) by A37, A15, XBOOLE_1:1, PRE_TOPC:7;
reconsider hBB = h " BB as Subset of M by A8, XBOOLE_1:1;
BB is open by TSEP_1:9;
then A39: h " BB is open by A9, TOPGRP_1:26;
W /\ (Ball ((0. (TOP-REAL n)),1)) c= h .: IU by A12, A11, TOPREAL9:16, XBOOLE_1:26;
then BB c= h .: IU by A35, A36;
then A40: h " BB c= h " (h .: IU) by RELAT_1:143;
h " (h .: IU) c= IU by FUNCT_1:82, A9;
then h " BB c= IU by A40;
then hBB is open by A39, TSEP_1:9;
then A41: Int hBB = hBB by TOPS_1:23;
A42: rng h = [#] (Tdisk ((0. (TOP-REAL n)),1)) by A9, TOPS_2:def 5;
then A43: h .: (h " BB) = BB by FUNCT_1:77;
not hBB is empty by A34, RELAT_1:139, A42;
then consider t being set such that
A44: t in hBB ;
reconsider t = t as Point of M by A44;
reconsider hBB = hBB as a_neighborhood of t by A41, CONNSP_2:def 1, A44;
A45: (TOP-REAL n) | (Ball (wb,s)) = Tball (wb,s) by MFOLD_1:def 2;
A46: (M | U) | (h " BB) = M | hBB by A8, PRE_TOPC:7;
then reconsider HH = h | (h " BB) as Function of (M | hBB),((TOP-REAL n) | (Ball (wb,s))) by A43, A38, JORDAN24:12;
HH is being_homeomorphism by A9, A43, A38, A46, METRIZTS:2;
then A47: 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 MFOLD_1:9, A34;
then M | hBB, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A47, A45, A34, BORSUK_3:3;
hence ( not Int M is empty & Int M is open ) by A1, TOPS_1:25, Def3; :: thesis: verum