let p1, p2, p3, p4 be Point of (TOP-REAL 2); for a, b, c, d being real number st a < b & c < d & p1 `1 = a & p2 `1 = a & p3 `2 = d & p4 `1 = b & c <= p1 `2 & p1 `2 < p2 `2 & p2 `2 <= d & a <= p3 `1 & p3 `1 <= b & c <= p4 `2 & p4 `2 <= d holds
p1,p2,p3,p4 are_in_this_order_on rectangle a,b,c,d
let a, b, c, d be real number ; ( a < b & c < d & p1 `1 = a & p2 `1 = a & p3 `2 = d & p4 `1 = b & c <= p1 `2 & p1 `2 < p2 `2 & p2 `2 <= d & a <= p3 `1 & p3 `1 <= b & c <= p4 `2 & p4 `2 <= d 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 `1 = b
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 <= b
and
A12:
c <= p4 `2
and
A13:
p4 `2 <= d
; p1,p2,p3,p4 are_in_this_order_on rectangle a,b,c,d
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, Th8;
hence
p1,p2,p3,p4 are_in_this_order_on rectangle a,b,c,d
by JORDAN17:def 1; verum