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