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