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