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

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

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

( x in Int M iff ex U being Subset of M st

( U is open & U c= Int M & x in U ) )

proof

set p = the Point of M;
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 ) )

( U is open & U c= Int M & x in U ) implies x in Int M ) ; :: thesis: verum

end;( 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 )

thus
( 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, Def4;

take W = Int U; :: thesis: ( W is open & W c= Int M & x in W )

W c= Int M

end;( 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, Def4;

take W = Int U; :: thesis: ( W is open & W c= Int M & x in W )

W c= Int M

proof

hence
( W is open & W c= Int M & x in W )
by CONNSP_2:def 1; :: thesis: verum
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 Def4, A3; :: thesis: verum

end;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 Def4, A3; :: thesis: verum

( U is open & U c= Int M & x in U ) implies x in Int M ) ; :: thesis: verum

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

proof

then consider wb being set such that
reconsider HP = hp as Point of (Euclid n) by EUCLID:67;

A16: Ball ((0. (TOP-REAL n)),1) misses Sphere ((0. (TOP-REAL n)),1) by TOPREAL9:19;

A17: cl_Ball ((0. (TOP-REAL n)),1) = (Ball ((0. (TOP-REAL n)),1)) \/ (Sphere ((0. (TOP-REAL n)),1)) by TOPREAL9:18;

assume A18: 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 A16, A17, XBOOLE_1:88 ;

then hp in Sphere ((0. (TOP-REAL n)),1) by A15, A13, XBOOLE_0:def 4;

then A19: |.hp.| = 1 by TOPREAL9:12;

Int W = W by TOPS_1:23;

then consider s being Real such that

A20: s > 0 and

A21: Ball (HP,s) c= W by A14, GOBOARD6:5;

set s2 = s / 2;

set m = min ((s / 2),(1 / 2));

A22: min ((s / 2),(1 / 2)) <= s / 2 by XXREAL_0:17;

s / 2 < s by A20, XREAL_1:216;

then A23: min ((s / 2),(1 / 2)) < s by A22, XXREAL_0:2;

A24: Ball (HP,s) = Ball (hp,s) by TOPREAL9:13;

A25: min ((s / 2),(1 / 2)) > 0 by A20, XXREAL_0:21;

then A26: 1 - (min ((s / 2),(1 / 2))) < 1 - 0 by XREAL_1:6;

A27: |.(- (min ((s / 2),(1 / 2)))).| = - (- (min ((s / 2),(1 / 2)))) by A25, ABSVALUE:def 1;

A28: ((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 A19, EUCLID:11;

then A29: (1 - (min ((s / 2),(1 / 2)))) * hp in Ball (hp,s) by A27, A23;

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 A19, EUCLID:11;

then (1 - (min ((s / 2),(1 / 2)))) * hp in Ball ((0. (TOP-REAL n)),1) by A28, A26;

hence contradiction by A29, A21, A24, A18, XBOOLE_0:def 4; :: thesis: verum

end;A16: Ball ((0. (TOP-REAL n)),1) misses Sphere ((0. (TOP-REAL n)),1) by TOPREAL9:19;

A17: cl_Ball ((0. (TOP-REAL n)),1) = (Ball ((0. (TOP-REAL n)),1)) \/ (Sphere ((0. (TOP-REAL n)),1)) by TOPREAL9:18;

assume A18: 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 A16, A17, XBOOLE_1:88 ;

then hp in Sphere ((0. (TOP-REAL n)),1) by A15, A13, XBOOLE_0:def 4;

then A19: |.hp.| = 1 by TOPREAL9:12;

Int W = W by TOPS_1:23;

then consider s being Real such that

A20: s > 0 and

A21: Ball (HP,s) c= W by A14, GOBOARD6:5;

set s2 = s / 2;

set m = min ((s / 2),(1 / 2));

A22: min ((s / 2),(1 / 2)) <= s / 2 by XXREAL_0:17;

s / 2 < s by A20, XREAL_1:216;

then A23: min ((s / 2),(1 / 2)) < s by A22, XXREAL_0:2;

A24: Ball (HP,s) = Ball (hp,s) by TOPREAL9:13;

A25: min ((s / 2),(1 / 2)) > 0 by A20, XXREAL_0:21;

then A26: 1 - (min ((s / 2),(1 / 2))) < 1 - 0 by XREAL_1:6;

A27: |.(- (min ((s / 2),(1 / 2)))).| = - (- (min ((s / 2),(1 / 2)))) by A25, ABSVALUE:def 1;

A28: ((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 A19, EUCLID:11;

then A29: (1 - (min ((s / 2),(1 / 2)))) * hp in Ball (hp,s) by A27, A23;

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 A19, EUCLID:11;

then (1 - (min ((s / 2),(1 / 2)))) * hp in Ball ((0. (TOP-REAL n)),1) by A28, A26;

hence contradiction by A29, A21, A24, A18, XBOOLE_0:def 4; :: thesis: verum

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