theorem Th27: :: JGRAPH_7:27

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