let I be Subset of M; :: thesis: ( I = Int M iff for p being Point of M holds
( p in I iff ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) )
thus ( I = Int M implies for p being Point of M holds
( p in I iff ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) ) :: thesis: ( ( for p being Point of M holds
( p in I iff ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) ) implies I = Int M )
proof
assume A1: I = Int M ; :: thesis: for p being Point of M holds
( p in I iff ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic )
let p be Point of M; :: thesis: ( p in I iff ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic )
thus ( p in I implies ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) :: thesis: ( ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic implies p in I )
proof
consider W being a_neighborhood of p such that
A2: M | W, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by Def3;
A3: p in Int W by CONNSP_2:def 1;
assume p in I ; :: thesis: ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
then consider U being a_neighborhood of p, m being Nat such that
A4: M | U, Tball ((0. (TOP-REAL m)),1) are_homeomorphic by A1, Def4;
p in Int U by CONNSP_2:def 1;
then n = m by A3, XBOOLE_0:3, A4, A2, BROUWER3:15;
hence ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A4; :: thesis: verum
end;
thus ( ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic implies p in I ) by Def4, A1; :: thesis: verum
end;
assume A6: for p being Point of M holds
( p in I iff ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) ; :: thesis: I = Int M
thus I c= Int M :: according to XBOOLE_0:def 10 :: thesis: Int M c= I
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in I or x in Int M )
assume A7: x in I ; :: thesis: x in Int M
then reconsider x = x as Point of M ;
ex U being a_neighborhood of x st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A7, A6;
hence x in Int M by Def4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Int M or x in I )
assume A8: x in Int M ; :: thesis: x in I
then reconsider x = x as Point of M ;
consider U being a_neighborhood of x, m being Nat such that
A9: M | U, Tball ((0. (TOP-REAL m)),1) are_homeomorphic by A8, Def4;
consider W being a_neighborhood of x such that
A11: M | W, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by Def3;
A12: x in Int W by CONNSP_2:def 1;
x in Int U by CONNSP_2:def 1;
then m = n by A12, XBOOLE_0:3, BROUWER3:15, A9, A11;
hence x in I by A6, A9; :: thesis: verum