let p1, p2 be Point of (TOP-REAL 2); :: thesis: for b, d being real number 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 number ; :: 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 A1: ( p2 `2 < d & p2 `2 <= p1 `2 & p1 `2 <= d & p1 `1 < p2 `1 & p2 `1 <= b ) ; :: thesis: LE p1,p2, rectangle (p1 `1 ),b,(p2 `2 ),d
then A2: p1 `1 < b by XXREAL_0:2;
then A3: ( p1 in LSeg |[(p1 `1 ),(p2 `2 )]|,|[(p1 `1 ),d]| & p2 in LSeg |[b,(p2 `2 )]|,|[(p1 `1 ),(p2 `2 )]| ) by A1, Th1, JGRAPH_6:10;
W-min (rectangle (p1 `1 ),b,(p2 `2 ),d) = |[(p1 `1 ),(p2 `2 )]| by A1, A2, JGRAPH_6:56;
then (W-min (rectangle (p1 `1 ),b,(p2 `2 ),d)) `1 = p1 `1 by EUCLID:56;
hence LE p1,p2, rectangle (p1 `1 ),b,(p2 `2 ),d by A1, A2, A3, JGRAPH_6:69; :: thesis: verum