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 & p2 `2 >= 0 & p3 `2 >= 0 & p4 `2 > 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 `1 < 0 & q1 `2 >= 0 & q2 `1 < 0 & q2 `2 >= 0 & q3 `1 < 0 & q3 `2 >= 0 & q4 `1 < 0 & q4 `2 >= 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )