let p1, p2 be Point of (TOP-REAL 2); :: thesis: for c, d being real number st p1 `1 < p2 `1 & c < d & c <= p1 `2 & p1 `2 <= d & c <= p2 `2 & p2 `2 <= d holds
LE p1,p2, rectangle (p1 `1 ),(p2 `1 ),c,d
let c, d be real number ; :: thesis: ( p1 `1 < p2 `1 & c < d & c <= p1 `2 & p1 `2 <= d & c <= p2 `2 & p2 `2 <= d implies LE p1,p2, rectangle (p1 `1 ),(p2 `1 ),c,d )
set a = p1 `1 ;
set b = p2 `1 ;
set K = rectangle (p1 `1 ),(p2 `1 ),c,d;
assume A1: ( p1 `1 < p2 `1 & c < d & c <= p1 `2 & p1 `2 <= d & c <= p2 `2 & p2 `2 <= d ) ; :: thesis: LE p1,p2, rectangle (p1 `1 ),(p2 `1 ),c,d
then A2: p1 in LSeg |[(p1 `1 ),c]|,|[(p1 `1 ),d]| by JGRAPH_6:10;
p2 in LSeg |[(p2 `1 ),c]|,|[(p2 `1 ),d]| by A1, JGRAPH_6:10;
hence LE p1,p2, rectangle (p1 `1 ),(p2 `1 ),c,d by A1, A2, JGRAPH_6:69; :: thesis: verum