theorem Th61:
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,d]|,
|[b,c]|) holds
(
LE p1,
p2,
rectangle (
a,
b,
c,
d) iff ( (
p2 in LSeg (
|[b,d]|,
|[b,c]|) &
p1 `2 >= p2 `2 ) or (
p2 in LSeg (
|[b,c]|,
|[a,c]|) &
p2 <> W-min (rectangle (a,b,c,d)) ) ) )