let a, b, c, d be Real; :: thesis: ( 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 ; :: thesis: ( (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 ;
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 ;
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 ; :: thesis: verum