let p1, p2 be Point of (TOP-REAL 2); for b, c, d being Real 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; ( 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 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
; 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:2;
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:2;
hence
LE p1,p2, rectangle ((p1 `1),b,c,d)
by A1, A4, A7, A8, JGRAPH_6:55; verum