let p1, p2 be Point of (TOP-REAL 2); :: thesis: for a, b, c, d being real number st a < b & c < d & p1 `1 = b & p2 `1 = b & c <= p2 `2 & p2 `2 < p1 `2 & p1 `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 `1 = b & p2 `1 = b & c <= p2 `2 & p2 `2 < p1 `2 & p1 `2 <= d implies LE p1,p2, rectangle a,b,c,d )
set K = rectangle a,b,c,d;
assume that
A1: a < b and
A2: c < d and
A3: p1 `1 = b and
A4: p2 `1 = b and
A5: c <= p2 `2 and
A6: p2 `2 < p1 `2 and
A7: p1 `2 <= d ; :: thesis: LE p1,p2, rectangle a,b,c,d
d >= p2 `2 by A6, A7, XXREAL_0:2;
then A8: p2 in LSeg |[b,d]|,|[b,c]| by A2, A4, A5, JGRAPH_6:10;
p1 `2 >= c by A5, A6, XXREAL_0:2;
then p1 in LSeg |[b,d]|,|[b,c]| by A2, A3, A7, JGRAPH_6:10;
hence LE p1,p2, rectangle a,b,c,d by A1, A2, A6, A8, JGRAPH_6:71; :: thesis: verum