let a, b, c, d be real number ; ( a < b & c < d implies ( (LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|) is_an_arc_of W-min (rectangle a,b,c,d), E-max (rectangle a,b,c,d) & (LSeg |[a,c]|,|[b,c]|) \/ (LSeg |[b,c]|,|[b,d]|) is_an_arc_of E-max (rectangle a,b,c,d), W-min (rectangle a,b,c,d) ) )
set K = rectangle a,b,c,d;
assume that
A1:
a < b
and
A2:
c < d
; ( (LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|) is_an_arc_of W-min (rectangle a,b,c,d), E-max (rectangle a,b,c,d) & (LSeg |[a,c]|,|[b,c]|) \/ (LSeg |[b,c]|,|[b,d]|) is_an_arc_of E-max (rectangle a,b,c,d), W-min (rectangle a,b,c,d) )
A3:
W-min (rectangle a,b,c,d) = |[a,c]|
by A1, A2, Th56;
A4:
E-max (rectangle a,b,c,d) = |[b,d]|
by A1, A2, Th56;
|[a,c]| `2 = c
by EUCLID:56;
then A5:
|[a,c]| <> |[a,d]|
by A2, EUCLID:56;
set p1 = |[a,c]|;
set p2 = |[a,d]|;
set q1 = |[b,d]|;
A6:
(LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,d]|,|[b,d]|) = {|[a,d]|}
by A1, A2, Th44;
|[a,c]| `1 = a
by EUCLID:56;
then A7:
|[a,c]| <> |[b,c]|
by A1, EUCLID:56;
set q2 = |[b,c]|;
(LSeg |[b,d]|,|[b,c]|) /\ (LSeg |[b,c]|,|[a,c]|) = {|[b,c]|}
by A1, A2, Th42;
hence
( (LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|) is_an_arc_of W-min (rectangle a,b,c,d), E-max (rectangle a,b,c,d) & (LSeg |[a,c]|,|[b,c]|) \/ (LSeg |[b,c]|,|[b,d]|) is_an_arc_of E-max (rectangle a,b,c,d), W-min (rectangle a,b,c,d) )
by A3, A4, A5, A6, A7, TOPREAL1:18; verum