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. ()),1) are_homeomorphic by ;
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 ;
hence y in Int M by ; :: 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
A5: M | U, Tdisk ((0. ()),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. ()),1)) such that
A7: h is being_homeomorphism by ;
IU is open by TSEP_1:9;
then h .: IU is open by ;
then h .: IU in the topology of (Tdisk ((0. ()),1)) by PRE_TOPC:def 2;
then consider W being Subset of () such that
A8: W in the topology of () and
A9: h .: IU = W /\ ([#] (Tdisk ((0. ()),1))) by PRE_TOPC:def 4;
A10: [#] (Tdisk ((0. ()),1)) = cl_Ball ((0. ()),1) by PRE_TOPC:def 5;
A11: dom h = [#] (M | U) by ;
A12: Ball ((0. ()),1) c= cl_Ball ((0. ()),1) by TOPREAL9:16;
reconsider W = W as open Subset of () by ;
set WB = W /\ (Ball ((0. ()),1));
the Point of M in Int U by CONNSP_2:def 1;
then A13: h . the Point of M in h .: IU by ;
then A14: h . the Point of M in W by ;
then reconsider hp = h . the Point of M as Point of () ;
A15: h .: IU = W /\ (cl_Ball ((0. ()),1)) by ;
not W /\ (Ball ((0. ()),1)) is empty
proof
reconsider HP = hp as Point of () by EUCLID:67;
A16: Ball ((0. ()),1) misses Sphere ((0. ()),1) by TOPREAL9:19;
A17: cl_Ball ((0. ()),1) = (Ball ((0. ()),1)) \/ (Sphere ((0. ()),1)) by TOPREAL9:18;
assume A18: W /\ (Ball ((0. ()),1)) is empty ; :: thesis: contradiction
then W /\ (cl_Ball ((0. ()),1)) = (W /\ (cl_Ball ((0. ()),1))) \ (W /\ (Ball ((0. ()),1)))
.= ((W /\ (cl_Ball ((0. ()),1))) \ W) \/ ((W /\ (cl_Ball ((0. ()),1))) \ (Ball ((0. ()),1))) by XBOOLE_1:54
.= {} \/ ((W /\ (cl_Ball ((0. ()),1))) \ (Ball ((0. ()),1))) by
.= W /\ ((cl_Ball ((0. ()),1)) \ (Ball ((0. ()),1))) by XBOOLE_1:49
.= W /\ (Sphere ((0. ()),1)) by ;
then hp in Sphere ((0. ()),1) by ;
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 ;
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 ;
then A23: min ((s / 2),(1 / 2)) < s by ;
A24: Ball (HP,s) = Ball (hp,s) by TOPREAL9:13;
A25: min ((s / 2),(1 / 2)) > 0 by ;
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 ;
A28: ((1 - (min ((s / 2),(1 / 2)))) * hp) - (0. ()) = (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 ;
then A29: (1 - (min ((s / 2),(1 / 2)))) * hp in Ball (hp,s) by ;
1 - (min ((s / 2),(1 / 2))) >= 1 - (1 / 2) by ;
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 ;
then (1 - (min ((s / 2),(1 / 2)))) * hp in Ball ((0. ()),1) by ;
hence contradiction by A29, A21, A24, A18, XBOOLE_0:def 4; :: thesis: verum
end;
then consider wb being set such that
A30: wb in W /\ (Ball ((0. ()),1)) ;
reconsider wb = wb as Point of () by A30;
reconsider wbE = wb as Point of () by EUCLID:67;
Int (W /\ (Ball ((0. ()),1))) = W /\ (Ball ((0. ()),1)) by TOPS_1:23;
then consider s being Real such that
A31: s > 0 and
A32: Ball (wbE,s) c= W /\ (Ball ((0. ()),1)) by ;
A33: Ball (wb,s) = Ball (wbE,s) by TOPREAL9:13;
W /\ (Ball ((0. ()),1)) c= Ball ((0. ()),1) by XBOOLE_1:17;
then A34: Ball (wb,s) c= Ball ((0. ()),1) by ;
then reconsider BB = Ball (wb,s) as Subset of (Tdisk ((0. ()),1)) by ;
A35: (Tdisk ((0. ()),1)) | BB = () | (Ball (wb,s)) by ;
reconsider hBB = h " BB as Subset of M by ;
BB is open by TSEP_1:9;
then A36: h " BB is open by ;
W /\ (Ball ((0. ()),1)) c= h .: IU by ;
then BB c= h .: IU by ;
then A37: h " BB c= h " (h .: IU) by RELAT_1:143;
h " (h .: IU) c= IU by ;
then h " BB c= IU by A37;
then hBB is open by ;
then A38: Int hBB = hBB by TOPS_1:23;
A39: rng h = [#] (Tdisk ((0. ()),1)) by ;
then A40: h .: (h " BB) = BB by FUNCT_1:77;
not hBB is empty by ;
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 ;
A43: (M | U) | (h " BB) = M | hBB by ;
then reconsider HH = h | (h " BB) as Function of (M | hBB),(() | (Ball (wb,s))) by ;
HH is being_homeomorphism by ;
then A44: M | hBB,() | (Ball (wb,s)) are_homeomorphic by T_0TOPSP:def 1;
Tball (wb,s), Tball ((0. ()),1) are_homeomorphic by ;
then M | hBB, Tball ((0. ()),1) are_homeomorphic by ;
hence ( not Int M is empty & Int M is open ) by ; :: thesis: verum