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

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 object ; :: 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 :: thesis:

assume p in LSeg (|[a,c]|,|[a,d]|) ; :: thesis:
then p `1 = a by TOPREAL3:11;
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:12;
then x = |[((a + b) / 2),d]| by A13, A14, EUCLID:53;
hence x in {|[((a + b) / 2),d]|} by TARSKI:def 1; :: thesis:

end;

let x be object ; :: 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: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:

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 object ; :: 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 :: thesis:

assume p in LSeg (|[b,c]|,|[b,d]|) ; :: thesis:
then p `1 = b by TOPREAL3:11;
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:12;
then x = |[((a + b) / 2),c]| by A24, A25, EUCLID:53;
hence x in {|[((a + b) / 2),c]|} by TARSKI:def 1; :: thesis:

end;

let x be object ; :: 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: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 |[((b + a) / 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:

end;