let a, b, c, d be real number ; :: thesis:
set K = rectangle a,b,c,d;
assume that
A1: a < b and
A2: c < d ; :: thesis:
A3: rectangle a,b,c,d is being_simple_closed_curve by A1, A2, Th60;
set P = rectangle a,b,c,d;
A4: W-min (rectangle a,b,c,d) = |[a,c]| by A1, A2, Th56;
A5: E-max (rectangle a,b,c,d) = |[b,d]| by A1, A2, Th56;
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, Th57;
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, Th57;
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 Th58;
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, Th46
.= Vertical_Line ((a + b) / 2) by A1, A2, Th48 ;
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 by XREAL_0:def 1;
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:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A11: x in U /\ (Vertical_Line (((W-bound (rectangle a,b,c,d)) + (E-bound (rectangle a,b,c,d))) / 2)) ; :: thesis:
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

assume p in LSeg |[a,c]|,|[a,d]| ; :: thesis:
then p `1 = a by TOPREAL3:17;
hence contradiction by A1, A14; :: thesis:

end;

then p in LSeg |[a2,d2]|,|[b2,d2]| by A12, A13, XBOOLE_0:def 3;
then p `2 = d by TOPREAL3:18;
then x = |[((a + b) / 2),d]| by A13, A14, EUCLID:57;
hence x in {|[((a + b) / 2),d]|} by TARSKI:def 1; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {|[((a + b) / 2),d]|} ; :: thesis:
then A15: x = |[((a + b) / 2),d]| by TARSKI:def 1;
|[((a + b) / 2),d]| `1 = (a + b) / 2 by EUCLID:56;
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:56;
A18: |[b,d]| `2 = d by EUCLID:56;
A19: |[a,d]| `1 = a by EUCLID:56;
|[a,d]| `2 = d by EUCLID:56;
then x in LSeg |[b,d]|,|[a,d]| by A1, A15, A17, A18, A19, TOPREAL3:19;
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:

end;

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:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A22: x in P3 /\ (Vertical_Line (((W-bound (rectangle a,b,c,d)) + (E-bound (rectangle a,b,c,d))) / 2)) ; :: thesis:
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

assume p in LSeg |[b,c]|,|[b,d]| ; :: thesis:
then p `1 = b by TOPREAL3:17;
hence contradiction by A1, A25; :: thesis:

end;

then p in LSeg |[a2,c2]|,|[b2,c2]| by A23, A24, XBOOLE_0:def 3;
then p `2 = c by TOPREAL3:18;
then x = |[((a + b) / 2),c]| by A24, A25, EUCLID:57;
hence x in {|[((a + b) / 2),c]|} by TARSKI:def 1; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {|[((a + b) / 2),c]|} ; :: thesis:
then A26: x = |[((a + b) / 2),c]| by TARSKI:def 1;
|[((a + b) / 2),c]| `1 = (a + b) / 2 by EUCLID:56;
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:56;
A29: |[b,c]| `2 = c by EUCLID:56;
A30: |[a,c]| `1 = a by EUCLID:56;
|[a,c]| `2 = c by EUCLID:56;
then |[((b + a) / 2),c]| in LSeg |[a,c]|,|[b,c]| by A1, A28, A29, A30, TOPREAL3:19;
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:

end;