let p1, p2 be Point of (TOP-REAL 2); for b, c being Real 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; ( 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 ;
assume that
A1:
p1 `1 < b
and
A2:
c < p2 `2
and
A3:
c <= p1 `2
and
A4:
p1 `2 <= p2 `2
and
A5:
p1 `1 <= p2 `1
and
A6:
p2 `1 <= b
; LE p1,p2, rectangle ((p1 `1),b,c,(p2 `2))
A7:
p1 in LSeg (|[(p1 `1),c]|,|[(p1 `1),(p2 `2)]|)
by A2, A3, A4, JGRAPH_6:2;
p2 in LSeg (|[(p1 `1),(p2 `2)]|,|[b,(p2 `2)]|)
by A1, A5, A6, Th1;
hence
LE p1,p2, rectangle ((p1 `1),b,c,(p2 `2))
by A1, A2, A7, JGRAPH_6:59; verum