let p1, p2, p3, p4 be Point of (TOP-REAL 2); ( p1 `1 <> p3 `1 & p4 `2 <> p2 `2 & p4 `2 <= p1 `2 & p1 `2 <= p2 `2 & p1 `1 <= p2 `1 & p2 `1 <= p3 `1 & p4 `2 <= p3 `2 & p3 `2 <= p2 `2 & p1 `1 < p4 `1 & p4 `1 <= p3 `1 implies p1,p2,p3,p4 are_in_this_order_on rectangle ((p1 `1),(p3 `1),(p4 `2),(p2 `2)) )
set K = rectangle ((p1 `1),(p3 `1),(p4 `2),(p2 `2));
assume that
A1:
p1 `1 <> p3 `1
and
A2:
p4 `2 <> p2 `2
and
A3:
p4 `2 <= p1 `2
and
A4:
p1 `2 <= p2 `2
and
A5:
p1 `1 <= p2 `1
and
A6:
p2 `1 <= p3 `1
and
A7:
p4 `2 <= p3 `2
and
A8:
p3 `2 <= p2 `2
and
A9:
p1 `1 < p4 `1
and
A10:
p4 `1 <= p3 `1
; p1,p2,p3,p4 are_in_this_order_on rectangle ((p1 `1),(p3 `1),(p4 `2),(p2 `2))
p4 `2 <= p2 `2
by A3, A4, XXREAL_0:2;
then A11:
p4 `2 < p2 `2
by A2, XXREAL_0:1;
p1 `1 <= p3 `1
by A5, A6, XXREAL_0:2;
then
p1 `1 < p3 `1
by A1, XXREAL_0:1;
then
( ( LE p1,p2, rectangle ((p1 `1),(p3 `1),(p4 `2),(p2 `2)) & LE p2,p3, rectangle ((p1 `1),(p3 `1),(p4 `2),(p2 `2)) & LE p3,p4, rectangle ((p1 `1),(p3 `1),(p4 `2),(p2 `2)) ) or ( LE p2,p3, rectangle ((p1 `1),(p3 `1),(p4 `2),(p2 `2)) & LE p3,p4, rectangle ((p1 `1),(p3 `1),(p4 `2),(p2 `2)) & LE p4,p1, rectangle ((p1 `1),(p3 `1),(p4 `2),(p2 `2)) ) or ( LE p3,p4, rectangle ((p1 `1),(p3 `1),(p4 `2),(p2 `2)) & LE p4,p1, rectangle ((p1 `1),(p3 `1),(p4 `2),(p2 `2)) & LE p1,p2, rectangle ((p1 `1),(p3 `1),(p4 `2),(p2 `2)) ) or ( LE p4,p1, rectangle ((p1 `1),(p3 `1),(p4 `2),(p2 `2)) & LE p1,p2, rectangle ((p1 `1),(p3 `1),(p4 `2),(p2 `2)) & LE p2,p3, rectangle ((p1 `1),(p3 `1),(p4 `2),(p2 `2)) ) )
by A3, A4, A5, A6, A7, A8, A9, A10, A11, Th4, Th8, Th11;
hence
p1,p2,p3,p4 are_in_this_order_on rectangle ((p1 `1),(p3 `1),(p4 `2),(p2 `2))
by JORDAN17:def 1; verum