theorem Th62: :: JGRAPH_6:62

for a, b, c, d being Real
for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[b,c]|,|[a,c]|) & p1 <> W-min (rectangle (a,b,c,d)) holds
( LE p1,p2, rectangle (a,b,c,d) iff ( p2 in LSeg (|[b,c]|,|[a,c]|) & p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) )