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. ()),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. ()),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. ()),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. ()),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. ()),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. ()),1) ) ) ) implies F = Fr M )
proof
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. ()),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. ()),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. ()),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. ()),1) ) )

thus ( p in F implies ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. ()),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. ()),1) ) ) :: thesis: ( ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. ()),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. ()),1) ) implies p in F )
proof
consider W being a_neighborhood of p such that
A2: M | W, Tdisk ((0. ()),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. ()),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. ()),1) )

then consider U being a_neighborhood of p, m being Nat, h being Function of (M | U),(Tdisk ((0. ()),1)) such that
A4: h is being_homeomorphism and
A5: h . p in Sphere ((0. ()),1) by ;
A6: p in Int U by CONNSP_2:def 1;
M | U, Tdisk ((0. ()),1) are_homeomorphic by ;
then n = m by ;
hence ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. ()),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. ()),1) ) by A4, A5; :: thesis: verum
end;
thus ( ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. ()),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. ()),1) ) implies p in F ) by ; :: thesis: verum
end;
assume A7: 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. ()),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. ()),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 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. ()),1)) st
( h is being_homeomorphism & h . x in Sphere ((0. ()),1) ) by A8, A7;
hence x in Fr M by Th5; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Fr M or x in 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. ()),1)) such that
A10: h is being_homeomorphism and
A11: h . x in Sphere ((0. ()),1) by ;
A12: x in Int U by CONNSP_2:def 1;
consider W being a_neighborhood of x such that
A13: M | W, Tdisk ((0. ()),1) are_homeomorphic by Def3;
A14: x in Int W by CONNSP_2:def 1;
M | U, Tdisk ((0. ()),1) are_homeomorphic by ;
then n = m by ;
hence x in F by A10, A11, A7; :: thesis: verum