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