let a, b, c, d be Real; ( 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, Th46;
A4:
E-max (rectangle (a,b,c,d)) = |[b,d]|
by A1, A2, Th46;
|[a,c]| `2 = c
by EUCLID:52;
then A5:
|[a,c]| <> |[a,d]|
by A2, EUCLID:52;
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, Th34;
|[a,c]| `1 = a
by EUCLID:52;
then A7:
|[a,c]| <> |[b,c]|
by A1, EUCLID:52;
set q2 = |[b,c]|;
(LSeg (|[b,d]|,|[b,c]|)) /\ (LSeg (|[b,c]|,|[a,c]|)) = {|[b,c]|}
by A1, A2, Th32;
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:12; verum