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