for p1, p2, p3, p4 being Point of (TOP-REAL 2) st p1 `1 <> p3 `1 & p4 `2 <> p2 `2 & p4 `2 <= p1 `2 & p1 `2 <= p2 `2 & p1 `1 <= p2 `1 & p2 `1 <= p3 `1 & p4 `2 <= p3 `2 & p3 `2 <= p2 `2 & p1 `1 < p4 `1 & p4 `1 <= p3 `1 holds
p1,p2,p3,p4 are_in_this_order_on rectangle ((p1 `1),(p3 `1),(p4 `2),(p2 `2))