let p1, p2 be Point of (TOP-REAL 2); :: thesis: for c, d being Real 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; :: 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 ;
assume that
A1: p1 `1 < p2 `1 and
A2: c < d and
A3: c <= p1 `2 and
A4: p1 `2 <= d and
A5: c <= p2 `2 and
A6: p2 `2 <= d ; :: thesis: LE p1,p2, rectangle ((p1 `1),(p2 `1),c,d)
A7: p2 in LSeg (|[(p2 `1),c]|,|[(p2 `1),d]|) by A2, A5, A6, JGRAPH_6:2;
p1 in LSeg (|[(p1 `1),c]|,|[(p1 `1),d]|) by A2, A3, A4, JGRAPH_6:2;
hence LE p1,p2, rectangle ((p1 `1),(p2 `1),c,d) by A1, A2, A7, JGRAPH_6:59; :: thesis: verum