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