set TR = TOP-REAL n;

let F be Subset of M; :: thesis: ( F = Fr M iff for p being Point of M holds

( p in F iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) ) )

thus ( F = Fr M implies for p being Point of M holds

( p in F iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) ) ) :: thesis: ( ( for p being Point of M holds

( p in F iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) ) ) implies F = Fr M )

( p in F iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) ) ; :: thesis: F = Fr M

thus F c= Fr M :: according to XBOOLE_0:def 10 :: thesis: Fr M c= F

assume A9: x in Fr M ; :: thesis: x in F

then reconsider x = x as Point of M ;

consider U being a_neighborhood of x, m being Nat, h being Function of (M | U),(Tdisk ((0. (TOP-REAL m)),1)) such that

A10: h is being_homeomorphism and

A11: h . x in Sphere ((0. (TOP-REAL m)),1) by A9, Th5;

A12: x in Int U by CONNSP_2:def 1;

consider W being a_neighborhood of x such that

A13: M | W, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by Def3;

A14: x in Int W by CONNSP_2:def 1;

M | U, Tdisk ((0. (TOP-REAL m)),1) are_homeomorphic by A10, T_0TOPSP:def 1;

then n = m by A14, A12, XBOOLE_0:3, A13, BROUWER3:14;

hence x in F by A10, A11, A7; :: thesis: verum

let F be Subset of M; :: thesis: ( F = Fr M iff for p being Point of M holds

( p in F iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) ) )

thus ( F = Fr M implies for p being Point of M holds

( p in F iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) ) ) :: thesis: ( ( for p being Point of M holds

( p in F iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) ) ) implies F = Fr M )

proof

assume A7:
for p being Point of M holds
assume A1:
F = Fr M
; :: thesis: for p being Point of M holds

( p in F iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) )

let p be Point of M; :: thesis: ( p in F iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) )

thus ( p in F implies ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) ) :: thesis: ( ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) implies p in F )

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) implies p in F ) by Th5, A1; :: thesis: verum

end;( p in F iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) )

let p be Point of M; :: thesis: ( p in F iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) )

thus ( p in F implies ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) ) :: thesis: ( ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) implies p in F )

proof

thus
( ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
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 F ; :: thesis: ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) )

then consider U being a_neighborhood of p, m being Nat, h being Function of (M | U),(Tdisk ((0. (TOP-REAL m)),1)) such that

A4: h is being_homeomorphism and

A5: h . p in Sphere ((0. (TOP-REAL m)),1) by A1, Th5;

A6: p in Int U by CONNSP_2:def 1;

M | U, Tdisk ((0. (TOP-REAL m)),1) are_homeomorphic by A4, T_0TOPSP:def 1;

then n = m by A3, A6, XBOOLE_0:3, A2, BROUWER3:14;

hence ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) by A4, A5; :: thesis: verum

end;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 F ; :: thesis: ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) )

then consider U being a_neighborhood of p, m being Nat, h being Function of (M | U),(Tdisk ((0. (TOP-REAL m)),1)) such that

A4: h is being_homeomorphism and

A5: h . p in Sphere ((0. (TOP-REAL m)),1) by A1, Th5;

A6: p in Int U by CONNSP_2:def 1;

M | U, Tdisk ((0. (TOP-REAL m)),1) are_homeomorphic by A4, T_0TOPSP:def 1;

then n = m by A3, A6, XBOOLE_0:3, A2, BROUWER3:14;

hence ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) by A4, A5; :: thesis: verum

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) implies p in F ) by Th5, A1; :: thesis: verum

( p in F iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) ) ; :: thesis: F = Fr M

thus F c= Fr M :: according to XBOOLE_0:def 10 :: thesis: Fr M c= F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Fr M or x in F )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in Fr M )

assume A8: x in F ; :: thesis: x in Fr M

then reconsider x = x as Point of M ;

ex U being a_neighborhood of x ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . x in Sphere ((0. (TOP-REAL n)),1) ) by A8, A7;

hence x in Fr M by Th5; :: thesis: verum

end;assume A8: x in F ; :: thesis: x in Fr M

then reconsider x = x as Point of M ;

ex U being a_neighborhood of x ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h . x in Sphere ((0. (TOP-REAL n)),1) ) by A8, A7;

hence x in Fr M by Th5; :: thesis: verum

assume A9: x in Fr M ; :: thesis: x in F

then reconsider x = x as Point of M ;

consider U being a_neighborhood of x, m being Nat, h being Function of (M | U),(Tdisk ((0. (TOP-REAL m)),1)) such that

A10: h is being_homeomorphism and

A11: h . x in Sphere ((0. (TOP-REAL m)),1) by A9, Th5;

A12: x in Int U by CONNSP_2:def 1;

consider W being a_neighborhood of x such that

A13: M | W, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by Def3;

A14: x in Int W by CONNSP_2:def 1;

M | U, Tdisk ((0. (TOP-REAL m)),1) are_homeomorphic by A10, T_0TOPSP:def 1;

then n = m by A14, A12, XBOOLE_0:3, A13, BROUWER3:14;

hence x in F by A10, A11, A7; :: thesis: verum