for p1, p2 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 } & p1 in P & p2 in P & p1 `1 > 0 & p2 `1 > 0 & p1 `2 < 0 & p2 `2 < 0 & ( p1 `1 >= p2 `1 or p1 `2 >= p2 `2 ) holds
LE p1,p2,P