theorem Th3: :: JGRAPH_4:3

for f being Function of (TOP-REAL 2),(TOP-REAL 2) st f is continuous & f is one-to-one & rng f = [#] (TOP-REAL 2) & ( for p2 being Point of (TOP-REAL 2) ex K being non empty compact Subset of (TOP-REAL 2) st
( K = f .: K & ex V2 being Subset of (TOP-REAL 2) st
( p2 in V2 & V2 is open & V2 c= K & f . p2 in V2 ) ) ) holds
f is being_homeomorphism