theorem Th62: :: JGRAPH_5:62

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 `2 >= 0 or p1 `1 >= 0 ) & ( p2 `2 >= 0 or p2 `1 >= 0 ) & ( p3 `2 >= 0 or p3 `1 >= 0 ) & ( p4 `2 > 0 or p4 `1 > 0 ) holds
ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `2 >= 0 & q2 `2 >= 0 & q3 `2 >= 0 & q4 `2 > 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )