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 () ;
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 () ;
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 () ;
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
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))
proof
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 ;
then x in { p where p is Point of () : p `1 = (a + b) / 2 } by ;
then consider p being Point of () such that
A13: x = p and
A14: p `1 = (a + b) / 2 ;
now :: thesis: not p in LSeg (|[a,c]|,|[a,d]|)end;
then p in LSeg (|[a2,d2]|,|[b2,d2]|) by ;
then p `2 = d by TOPREAL3:12;
then x = |[((a + b) / 2),d]| by ;
hence x in {|[((a + b) / 2),d]|} by TARSKI:def 1; :: thesis: verum
end;
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)) )
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 () : 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 ;
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 ;
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 ; :: thesis: verum
end;
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;
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 ;
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
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))
proof
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 ;
then x in { p where p is Point of () : p `1 = (a + b) / 2 } by ;
then consider p being Point of () such that
A24: x = p and
A25: p `1 = (a + b) / 2 ;
now :: thesis: not p in LSeg (|[b,c]|,|[b,d]|)end;
then p in LSeg (|[a2,c2]|,|[b2,c2]|) by ;
then p `2 = c by TOPREAL3:12;
then x = |[((a + b) / 2),c]| by ;
hence x in {|[((a + b) / 2),c]|} by TARSKI:def 1; :: thesis: verum
end;
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)) )
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 () : 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 ;
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 ;
then x in P3 by ;
hence x in P3 /\ (Vertical_Line (((W-bound (rectangle (a,b,c,d))) + (E-bound (rectangle (a,b,c,d)))) / 2)) by ; :: thesis: verum
end;
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;
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 ;
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 ; :: thesis: verum