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