theorem Th67: :: JGRAPH_5:67

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & p1 <> p2 & p2 <> p3 & p3 <> p4 holds
ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & |[(- 1),0]| = f . p1 & |[0,1]| = f . p2 & |[1,0]| = f . p3 & |[0,(- 1)]| = f . p4 )