let p1, p2 be Point of (TOP-REAL 2); for a, b, c, d being Real st a < b & c < d & p1 `2 = d & p2 `2 = c & a <= p1 `1 & p1 `1 <= b & a < p2 `1 & p2 `1 <= b holds
LE p1,p2, rectangle (a,b,c,d)
let a, b, c, d be Real; ( a < b & c < d & p1 `2 = d & p2 `2 = c & a <= p1 `1 & p1 `1 <= b & a < p2 `1 & p2 `1 <= b implies LE p1,p2, rectangle (a,b,c,d) )
set K = rectangle (a,b,c,d);
assume that
A1:
a < b
and
A2:
c < d
and
A3:
p1 `2 = d
and
A4:
p2 `2 = c
and
A5:
a <= p1 `1
and
A6:
p1 `1 <= b
and
A7:
a < p2 `1
and
A8:
p2 `1 <= b
; LE p1,p2, rectangle (a,b,c,d)
A9:
p2 in LSeg (|[b,c]|,|[a,c]|)
by A1, A4, A7, A8, Th1;
W-min (rectangle (a,b,c,d)) = |[a,c]|
by A1, A2, JGRAPH_6:46;
then A10:
(W-min (rectangle (a,b,c,d))) `1 = a
by EUCLID:52;
p1 in LSeg (|[a,d]|,|[b,d]|)
by A1, A3, A5, A6, Th1;
hence
LE p1,p2, rectangle (a,b,c,d)
by A1, A2, A7, A9, A10, JGRAPH_6:60; verum