let n be Nat; :: thesis: for A, B being Subset of () st n = 0 holds
for h being Function of (() | A),(() | B) st h is being_homeomorphism holds
for p being Point of () holds
( ( p in Fr A implies h . p in Fr B ) & ( p in Int A implies h . p in Int B ) )

set TR = TOP-REAL n;
A1: Int ([#] ()) = [#] () by TOPS_1:15;
let A, B be Subset of (); :: thesis: ( n = 0 implies for h being Function of (() | A),(() | B) st h is being_homeomorphism holds
for p being Point of () holds
( ( p in Fr A implies h . p in Fr B ) & ( p in Int A implies h . p in Int B ) ) )

assume A2: n = 0 ; :: thesis: for h being Function of (() | A),(() | B) st h is being_homeomorphism holds
for p being Point of () holds
( ( p in Fr A implies h . p in Fr B ) & ( p in Int A implies h . p in Int B ) )

A3: the carrier of () = {(0. ())} by ;
let h be Function of (() | A),(() | B); :: thesis: ( h is being_homeomorphism implies for p being Point of () holds
( ( p in Fr A implies h . p in Fr B ) & ( p in Int A implies h . p in Int B ) ) )

assume A4: h is being_homeomorphism ; :: thesis: for p being Point of () holds
( ( p in Fr A implies h . p in Fr B ) & ( p in Int A implies h . p in Int B ) )

A5: dom h = [#] (() | A) by ;
let p be Point of (); :: thesis: ( ( p in Fr A implies h . p in Fr B ) & ( p in Int A implies h . p in Int B ) )
[#] () is open ;
hence ( p in Fr A implies h . p in Fr B ) by ; :: thesis: ( p in Int A implies h . p in Int B )
A6: A = [#] (() | A) by PRE_TOPC:def 5;
A7: Int A c= A by TOPS_1:16;
assume p in Int A ; :: thesis: h . p in Int B
then A8: h . p in rng h by ;
A9: B = [#] (() | B) by PRE_TOPC:def 5;
then B = [#] () by ;
hence h . p in Int B by A8, A1, A9; :: thesis: verum