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 = b & p3 `1 = b & p4 `2 = c & c <= p1 `2 & p1 `2 <= d & d >= p2 `2 & p2 `2 > p3 `2 & p3 `2 >= c & a < 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 = b & p3 `1 = b & p4 `2 = c & c <= p1 `2 & p1 `2 <= d & d >= p2 `2 & p2 `2 > p3 `2 & p3 `2 >= c & a < 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 = b
and
A5:
p3 `1 = b
and
A6:
p4 `2 = c
and
A7:
c <= p1 `2
and
A8:
p1 `2 <= d
and
A9:
d >= p2 `2
and
A10:
p2 `2 > p3 `2
and
A11:
p3 `2 >= c
and
A12:
a < p4 `1
and
A13:
p4 `1 <= b
; p1,p2,p3,p4 are_in_this_order_on rectangle (a,b,c,d)
A14:
p3 `2 < d
by A9, A10, XXREAL_0:2;
p2 `2 > c
by A10, A11, 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, A14, Th5, Th10, Th11;
hence
p1,p2,p3,p4 are_in_this_order_on rectangle (a,b,c,d)
by JORDAN17:def 1; verum