let p1, p2, p3, p4 be Point of (TOP-REAL 2); for a, b, c, d being Real st a < b & c < d & p1 `1 = a & p2 `1 = a & p3 `2 = d & p4 `2 = d & c <= p1 `2 & p1 `2 < p2 `2 & p2 `2 <= d & a <= p3 `1 & p3 `1 < p4 `1 & p4 `1 <= b holds
p1,p2,p3,p4 are_in_this_order_on rectangle (a,b,c,d)
let a, b, c, d be Real; ( a < b & c < d & p1 `1 = a & p2 `1 = a & p3 `2 = d & p4 `2 = d & c <= p1 `2 & p1 `2 < p2 `2 & p2 `2 <= d & a <= p3 `1 & p3 `1 < p4 `1 & p4 `1 <= b implies p1,p2,p3,p4 are_in_this_order_on rectangle (a,b,c,d) )
set K = rectangle (a,b,c,d);
assume that
A1:
a < b
and
A2:
c < d
and
A3:
p1 `1 = a
and
A4:
p2 `1 = a
and
A5:
p3 `2 = d
and
A6:
p4 `2 = d
and
A7:
c <= p1 `2
and
A8:
p1 `2 < p2 `2
and
A9:
p2 `2 <= d
and
A10:
a <= p3 `1
and
A11:
p3 `1 < p4 `1
and
A12:
p4 `1 <= b
; p1,p2,p3,p4 are_in_this_order_on rectangle (a,b,c,d)
A13:
p3 `1 < b
by A11, A12, XXREAL_0:2;
c < p2 `2
by A7, A8, XXREAL_0:2;
then
( ( LE p1,p2, rectangle (a,b,c,d) & LE p2,p3, rectangle (a,b,c,d) & LE p3,p4, rectangle (a,b,c,d) ) or ( LE p2,p3, rectangle (a,b,c,d) & LE p3,p4, rectangle (a,b,c,d) & LE p4,p1, rectangle (a,b,c,d) ) or ( LE p3,p4, rectangle (a,b,c,d) & LE p4,p1, rectangle (a,b,c,d) & LE p1,p2, rectangle (a,b,c,d) ) or ( LE p4,p1, rectangle (a,b,c,d) & LE p1,p2, rectangle (a,b,c,d) & LE p2,p3, rectangle (a,b,c,d) ) )
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, Th3, Th4, Th7;
hence
p1,p2,p3,p4 are_in_this_order_on rectangle (a,b,c,d)
by JORDAN17:def 1; verum