let p1, p2, p3, p4 be Point of (TOP-REAL 2); for a, b, c, d being Real st a < b & c < d & p1 `2 = d & p2 `1 = b & p3 `1 = b & p4 `1 = b & a <= p1 `1 & p1 `1 <= b & d >= p2 `2 & p2 `2 > p3 `2 & p3 `2 > p4 `2 & p4 `2 >= c 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 `2 = d & p2 `1 = b & p3 `1 = b & p4 `1 = b & a <= p1 `1 & p1 `1 <= b & d >= p2 `2 & p2 `2 > p3 `2 & p3 `2 > p4 `2 & p4 `2 >= c 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 `2 = d
and
A4:
p2 `1 = b
and
A5:
p3 `1 = b
and
A6:
p4 `1 = b
and
A7:
a <= p1 `1
and
A8:
p1 `1 <= b
and
A9:
d >= p2 `2
and
A10:
p2 `2 > p3 `2
and
A11:
p3 `2 > p4 `2
and
A12:
p4 `2 >= c
; p1,p2,p3,p4 are_in_this_order_on rectangle (a,b,c,d)
A13:
p3 `2 > c
by A11, A12, XXREAL_0:2;
p2 `2 > p4 `2
by A10, A11, XXREAL_0:2;
then A14:
p2 `2 > c
by A12, XXREAL_0:2;
d > p3 `2
by A9, A10, 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, A14, A13, Th8, Th10;
hence
p1,p2,p3,p4 are_in_this_order_on rectangle (a,b,c,d)
by JORDAN17:def 1; verum