let a, b, c, d be Real; :: thesis: ( a < b & c < d implies Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|)) )

set K = rectangle (a,b,c,d);

assume that

A1: a < b and

A2: c < d ; :: thesis: Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|))

A3: rectangle (a,b,c,d) is being_simple_closed_curve by A1, A2, Th50;

set P = rectangle (a,b,c,d);

A4: W-min (rectangle (a,b,c,d)) = |[a,c]| by A1, A2, Th46;

A5: E-max (rectangle (a,b,c,d)) = |[b,d]| by A1, A2, Th46;

reconsider U = (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) as non empty Subset of (TOP-REAL 2) ;

A6: U is_an_arc_of W-min (rectangle (a,b,c,d)), E-max (rectangle (a,b,c,d)) by A1, A2, Th47;

reconsider P3 = (LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|)) as non empty Subset of (TOP-REAL 2) ;

A7: P3 is_an_arc_of E-max (rectangle (a,b,c,d)), W-min (rectangle (a,b,c,d)) by A1, A2, Th47;

reconsider f1 = <*|[a,c]|,|[a,d]|,|[b,d]|*>, f2 = <*|[a,c]|,|[b,c]|,|[b,d]|*> as FinSequence of (TOP-REAL 2) ;

set p0 = |[a,c]|;

set p01 = |[a,d]|;

set p10 = |[b,c]|;

set p1 = |[b,d]|;

A8: ( a < b & c < d & |[a,c]| = |[a,c]| & |[b,d]| = |[b,d]| & |[a,d]| = |[a,d]| & |[b,c]| = |[b,c]| & f1 = <*|[a,c]|,|[a,d]|,|[b,d]|*> & f2 = <*|[a,c]|,|[b,c]|,|[b,d]|*> implies ( f1 is being_S-Seq & L~ f1 = (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) & f2 is being_S-Seq & L~ f2 = (LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|)) & rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[a,c]|,|[b,d]|} & f1 /. 1 = |[a,c]| & f1 /. (len f1) = |[b,d]| & f2 /. 1 = |[a,c]| & f2 /. (len f2) = |[b,d]| ) ) by Th48;

A9: Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2) = Vertical_Line ((a + (E-bound (rectangle (a,b,c,d)))) / 2) by A1, A2, Th36

.= Vertical_Line ((a + b) / 2) by A1, A2, Th38 ;

set Q = Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2);

reconsider a2 = a, b2 = b, c2 = c, d2 = d as Real ;

A10: U /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) = {|[((a + b) / 2),d]|}

then U meets Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2) ;

then First_Point (U,(W-min (rectangle (a,b,c,d))),(E-max (rectangle (a,b,c,d))),(Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2))) in {|[((a + b) / 2),d]|} by A6, A10, JORDAN5C:def 1;

then First_Point (U,(W-min (rectangle (a,b,c,d))),(E-max (rectangle (a,b,c,d))),(Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2))) = |[((a + b) / 2),d]| by TARSKI:def 1;

then A20: (First_Point (U,(W-min (rectangle (a,b,c,d))),(E-max (rectangle (a,b,c,d))),(Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)))) `2 = d by EUCLID:52;

A21: P3 /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) = {|[((a + b) / 2),c]|}

then P3 meets Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2) ;

then Last_Point (P3,(E-max (rectangle (a,b,c,d))),(W-min (rectangle (a,b,c,d))),(Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2))) in {|[((a + b) / 2),c]|} by A7, A21, JORDAN5C:def 2;

then Last_Point (P3,(E-max (rectangle (a,b,c,d))),(W-min (rectangle (a,b,c,d))),(Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2))) = |[((a + b) / 2),c]| by TARSKI:def 1;

then A31: (Last_Point (P3,(E-max (rectangle (a,b,c,d))),(W-min (rectangle (a,b,c,d))),(Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)))) `2 = c by EUCLID:52;

A32: P3 is_an_arc_of E-max (rectangle (a,b,c,d)), W-min (rectangle (a,b,c,d)) by A1, A2, Th47;

A33: (Upper_Arc (rectangle (a,b,c,d))) /\ P3 = {(W-min (rectangle (a,b,c,d))),(E-max (rectangle (a,b,c,d)))} by A1, A2, A4, A5, A8, Th51;

A34: (Upper_Arc (rectangle (a,b,c,d))) \/ P3 = rectangle (a,b,c,d) by A1, A2, A8, Th51;

(First_Point ((Upper_Arc (rectangle (a,b,c,d))),(W-min (rectangle (a,b,c,d))),(E-max (rectangle (a,b,c,d))),(Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)))) `2 > (Last_Point (P3,(E-max (rectangle (a,b,c,d))),(W-min (rectangle (a,b,c,d))),(Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)))) `2 by A1, A2, A20, A31, Th51;

hence Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|)) by A3, A32, A33, A34, JORDAN6:def 9; :: thesis: verum

set K = rectangle (a,b,c,d);

assume that

A1: a < b and

A2: c < d ; :: thesis: Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|))

A3: rectangle (a,b,c,d) is being_simple_closed_curve by A1, A2, Th50;

set P = rectangle (a,b,c,d);

A4: W-min (rectangle (a,b,c,d)) = |[a,c]| by A1, A2, Th46;

A5: E-max (rectangle (a,b,c,d)) = |[b,d]| by A1, A2, Th46;

reconsider U = (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) as non empty Subset of (TOP-REAL 2) ;

A6: U is_an_arc_of W-min (rectangle (a,b,c,d)), E-max (rectangle (a,b,c,d)) by A1, A2, Th47;

reconsider P3 = (LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|)) as non empty Subset of (TOP-REAL 2) ;

A7: P3 is_an_arc_of E-max (rectangle (a,b,c,d)), W-min (rectangle (a,b,c,d)) by A1, A2, Th47;

reconsider f1 = <*|[a,c]|,|[a,d]|,|[b,d]|*>, f2 = <*|[a,c]|,|[b,c]|,|[b,d]|*> as FinSequence of (TOP-REAL 2) ;

set p0 = |[a,c]|;

set p01 = |[a,d]|;

set p10 = |[b,c]|;

set p1 = |[b,d]|;

A8: ( a < b & c < d & |[a,c]| = |[a,c]| & |[b,d]| = |[b,d]| & |[a,d]| = |[a,d]| & |[b,c]| = |[b,c]| & f1 = <*|[a,c]|,|[a,d]|,|[b,d]|*> & f2 = <*|[a,c]|,|[b,c]|,|[b,d]|*> implies ( f1 is being_S-Seq & L~ f1 = (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) & f2 is being_S-Seq & L~ f2 = (LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|)) & rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[a,c]|,|[b,d]|} & f1 /. 1 = |[a,c]| & f1 /. (len f1) = |[b,d]| & f2 /. 1 = |[a,c]| & f2 /. (len f2) = |[b,d]| ) ) by Th48;

A9: Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2) = Vertical_Line ((a + (E-bound (rectangle (a,b,c,d)))) / 2) by A1, A2, Th36

.= Vertical_Line ((a + b) / 2) by A1, A2, Th38 ;

set Q = Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2);

reconsider a2 = a, b2 = b, c2 = c, d2 = d as Real ;

A10: U /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) = {|[((a + b) / 2),d]|}

proof

then
|[((a + b) / 2),d]| in U /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2))
by TARSKI:def 1;
thus
U /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) c= {|[((a + b) / 2),d]|}
:: according to XBOOLE_0:def 10 :: thesis: {|[((a + b) / 2),d]|} c= U /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2))

assume x in {|[((a + b) / 2),d]|} ; :: thesis: x in U /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2))

then A15: x = |[((a + b) / 2),d]| by TARSKI:def 1;

|[((a + b) / 2),d]| `1 = (a + b) / 2 by EUCLID:52;

then x in { p where p is Point of (TOP-REAL 2) : p `1 = (a + b) / 2 } by A15;

then A16: x in Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2) by A9, JORDAN6:def 6;

A17: |[b,d]| `1 = b by EUCLID:52;

A18: |[b,d]| `2 = d by EUCLID:52;

A19: |[a,d]| `1 = a by EUCLID:52;

|[a,d]| `2 = d by EUCLID:52;

then x in LSeg (|[b,d]|,|[a,d]|) by A1, A15, A17, A18, A19, TOPREAL3:13;

then x in U by XBOOLE_0:def 3;

hence x in U /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) by A16, XBOOLE_0:def 4; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {|[((a + b) / 2),d]|} or x in U /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in U /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) or x in {|[((a + b) / 2),d]|} )

assume A11: x in U /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) ; :: thesis: x in {|[((a + b) / 2),d]|}

then A12: x in U by XBOOLE_0:def 4;

x in Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2) by A11, XBOOLE_0:def 4;

then x in { p where p is Point of (TOP-REAL 2) : p `1 = (a + b) / 2 } by A9, JORDAN6:def 6;

then consider p being Point of (TOP-REAL 2) such that

A13: x = p and

A14: p `1 = (a + b) / 2 ;

then p `2 = d by TOPREAL3:12;

then x = |[((a + b) / 2),d]| by A13, A14, EUCLID:53;

hence x in {|[((a + b) / 2),d]|} by TARSKI:def 1; :: thesis: verum

end;assume A11: x in U /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) ; :: thesis: x in {|[((a + b) / 2),d]|}

then A12: x in U by XBOOLE_0:def 4;

x in Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2) by A11, XBOOLE_0:def 4;

then x in { p where p is Point of (TOP-REAL 2) : p `1 = (a + b) / 2 } by A9, JORDAN6:def 6;

then consider p being Point of (TOP-REAL 2) such that

A13: x = p and

A14: p `1 = (a + b) / 2 ;

now :: thesis: not p in LSeg (|[a,c]|,|[a,d]|)

then
p in LSeg (|[a2,d2]|,|[b2,d2]|)
by A12, A13, XBOOLE_0:def 3;assume
p in LSeg (|[a,c]|,|[a,d]|)
; :: thesis: contradiction

then p `1 = a by TOPREAL3:11;

hence contradiction by A1, A14; :: thesis: verum

end;then p `1 = a by TOPREAL3:11;

hence contradiction by A1, A14; :: thesis: verum

then p `2 = d by TOPREAL3:12;

then x = |[((a + b) / 2),d]| by A13, A14, EUCLID:53;

hence x in {|[((a + b) / 2),d]|} by TARSKI:def 1; :: thesis: verum

assume x in {|[((a + b) / 2),d]|} ; :: thesis: x in U /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2))

then A15: x = |[((a + b) / 2),d]| by TARSKI:def 1;

|[((a + b) / 2),d]| `1 = (a + b) / 2 by EUCLID:52;

then x in { p where p is Point of (TOP-REAL 2) : p `1 = (a + b) / 2 } by A15;

then A16: x in Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2) by A9, JORDAN6:def 6;

A17: |[b,d]| `1 = b by EUCLID:52;

A18: |[b,d]| `2 = d by EUCLID:52;

A19: |[a,d]| `1 = a by EUCLID:52;

|[a,d]| `2 = d by EUCLID:52;

then x in LSeg (|[b,d]|,|[a,d]|) by A1, A15, A17, A18, A19, TOPREAL3:13;

then x in U by XBOOLE_0:def 3;

hence x in U /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) by A16, XBOOLE_0:def 4; :: thesis: verum

then U meets Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2) ;

then First_Point (U,(W-min (rectangle (a,b,c,d))),(E-max (rectangle (a,b,c,d))),(Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2))) in {|[((a + b) / 2),d]|} by A6, A10, JORDAN5C:def 1;

then First_Point (U,(W-min (rectangle (a,b,c,d))),(E-max (rectangle (a,b,c,d))),(Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2))) = |[((a + b) / 2),d]| by TARSKI:def 1;

then A20: (First_Point (U,(W-min (rectangle (a,b,c,d))),(E-max (rectangle (a,b,c,d))),(Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)))) `2 = d by EUCLID:52;

A21: P3 /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) = {|[((a + b) / 2),c]|}

proof

then
|[((a + b) / 2),c]| in P3 /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2))
by TARSKI:def 1;
thus
P3 /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) c= {|[((a + b) / 2),c]|}
:: according to XBOOLE_0:def 10 :: thesis: {|[((a + b) / 2),c]|} c= P3 /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2))

assume x in {|[((a + b) / 2),c]|} ; :: thesis: x in P3 /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2))

then A26: x = |[((a + b) / 2),c]| by TARSKI:def 1;

|[((a + b) / 2),c]| `1 = (a + b) / 2 by EUCLID:52;

then x in { p where p is Point of (TOP-REAL 2) : p `1 = (a + b) / 2 } by A26;

then A27: x in Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2) by A9, JORDAN6:def 6;

A28: |[b,c]| `1 = b by EUCLID:52;

A29: |[b,c]| `2 = c by EUCLID:52;

A30: |[a,c]| `1 = a by EUCLID:52;

|[a,c]| `2 = c by EUCLID:52;

then |[((a + b) / 2),c]| in LSeg (|[a,c]|,|[b,c]|) by A1, A28, A29, A30, TOPREAL3:13;

then x in P3 by A26, XBOOLE_0:def 3;

hence x in P3 /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) by A27, XBOOLE_0:def 4; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {|[((a + b) / 2),c]|} or x in P3 /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P3 /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) or x in {|[((a + b) / 2),c]|} )

assume A22: x in P3 /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) ; :: thesis: x in {|[((a + b) / 2),c]|}

then A23: x in P3 by XBOOLE_0:def 4;

x in Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2) by A22, XBOOLE_0:def 4;

then x in { p where p is Point of (TOP-REAL 2) : p `1 = (a + b) / 2 } by A9, JORDAN6:def 6;

then consider p being Point of (TOP-REAL 2) such that

A24: x = p and

A25: p `1 = (a + b) / 2 ;

then p `2 = c by TOPREAL3:12;

then x = |[((a + b) / 2),c]| by A24, A25, EUCLID:53;

hence x in {|[((a + b) / 2),c]|} by TARSKI:def 1; :: thesis: verum

end;assume A22: x in P3 /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) ; :: thesis: x in {|[((a + b) / 2),c]|}

then A23: x in P3 by XBOOLE_0:def 4;

x in Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2) by A22, XBOOLE_0:def 4;

then x in { p where p is Point of (TOP-REAL 2) : p `1 = (a + b) / 2 } by A9, JORDAN6:def 6;

then consider p being Point of (TOP-REAL 2) such that

A24: x = p and

A25: p `1 = (a + b) / 2 ;

now :: thesis: not p in LSeg (|[b,c]|,|[b,d]|)

then
p in LSeg (|[a2,c2]|,|[b2,c2]|)
by A23, A24, XBOOLE_0:def 3;assume
p in LSeg (|[b,c]|,|[b,d]|)
; :: thesis: contradiction

then p `1 = b by TOPREAL3:11;

hence contradiction by A1, A25; :: thesis: verum

end;then p `1 = b by TOPREAL3:11;

hence contradiction by A1, A25; :: thesis: verum

then p `2 = c by TOPREAL3:12;

then x = |[((a + b) / 2),c]| by A24, A25, EUCLID:53;

hence x in {|[((a + b) / 2),c]|} by TARSKI:def 1; :: thesis: verum

assume x in {|[((a + b) / 2),c]|} ; :: thesis: x in P3 /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2))

then A26: x = |[((a + b) / 2),c]| by TARSKI:def 1;

|[((a + b) / 2),c]| `1 = (a + b) / 2 by EUCLID:52;

then x in { p where p is Point of (TOP-REAL 2) : p `1 = (a + b) / 2 } by A26;

then A27: x in Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2) by A9, JORDAN6:def 6;

A28: |[b,c]| `1 = b by EUCLID:52;

A29: |[b,c]| `2 = c by EUCLID:52;

A30: |[a,c]| `1 = a by EUCLID:52;

|[a,c]| `2 = c by EUCLID:52;

then |[((a + b) / 2),c]| in LSeg (|[a,c]|,|[b,c]|) by A1, A28, A29, A30, TOPREAL3:13;

then x in P3 by A26, XBOOLE_0:def 3;

hence x in P3 /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) by A27, XBOOLE_0:def 4; :: thesis: verum

then P3 meets Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2) ;

then Last_Point (P3,(E-max (rectangle (a,b,c,d))),(W-min (rectangle (a,b,c,d))),(Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2))) in {|[((a + b) / 2),c]|} by A7, A21, JORDAN5C:def 2;

then Last_Point (P3,(E-max (rectangle (a,b,c,d))),(W-min (rectangle (a,b,c,d))),(Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2))) = |[((a + b) / 2),c]| by TARSKI:def 1;

then A31: (Last_Point (P3,(E-max (rectangle (a,b,c,d))),(W-min (rectangle (a,b,c,d))),(Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)))) `2 = c by EUCLID:52;

A32: P3 is_an_arc_of E-max (rectangle (a,b,c,d)), W-min (rectangle (a,b,c,d)) by A1, A2, Th47;

A33: (Upper_Arc (rectangle (a,b,c,d))) /\ P3 = {(W-min (rectangle (a,b,c,d))),(E-max (rectangle (a,b,c,d)))} by A1, A2, A4, A5, A8, Th51;

A34: (Upper_Arc (rectangle (a,b,c,d))) \/ P3 = rectangle (a,b,c,d) by A1, A2, A8, Th51;

(First_Point ((Upper_Arc (rectangle (a,b,c,d))),(W-min (rectangle (a,b,c,d))),(E-max (rectangle (a,b,c,d))),(Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)))) `2 > (Last_Point (P3,(E-max (rectangle (a,b,c,d))),(W-min (rectangle (a,b,c,d))),(Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)))) `2 by A1, A2, A20, A31, Th51;

hence Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|)) by A3, A32, A33, A34, JORDAN6:def 9; :: thesis: verum