theorem :: JORDAN2B:28

for f being Function of (TOP-REAL 1),R^1 st ( for p being Element of (TOP-REAL 1) holds f . p = p /. 1 ) holds
f is being_homeomorphism