let P be Subset of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve implies ex P1, P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) )

assume P is being_simple_closed_curve ; :: thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )

then reconsider P = P as Simple_closed_curve ;

A1: W-min P in P by SPRECT_1:13;

A2: E-max P in P by SPRECT_1:14;

W-min P <> E-max P by TOPREAL5:19;

then consider P01, P02 being non empty Subset of (TOP-REAL 2) such that

A3: P01 is_an_arc_of W-min P, E-max P and

A4: P02 is_an_arc_of W-min P, E-max P and

A5: P = P01 \/ P02 and

A6: P01 /\ P02 = {(W-min P),(E-max P)} by A1, A2, TOPREAL2:5;

reconsider P01 = P01, P02 = P02 as non empty Subset of (TOP-REAL 2) ;

A7: P01 is_an_arc_of E-max P, W-min P by A3, JORDAN5B:14;

A8: P02 is_an_arc_of E-max P, W-min P by A4, JORDAN5B:14;

reconsider P001 = P01, P002 = P02 as non empty Subset of (TOP-REAL 2) ;

A9: (E-max P) `1 = E-bound P by EUCLID:52;

A10: Vertical_Line (((W-bound P) + (E-bound P)) / 2) is closed by Th6;

P01 is closed by A3, COMPTS_1:7, JORDAN5A:1;

then A11: P01 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed by A10, TOPS_1:8;

A12: Vertical_Line (((W-bound P) + (E-bound P)) / 2) is closed by Th6;

P02 is closed by A4, COMPTS_1:7, JORDAN5A:1;

then A13: P02 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed by A12, TOPS_1:8;

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

A14: q1 in P001 and

A15: q1 `1 = (((W-min P) `1) + ((E-max P) `1)) / 2 by A3, Th12;

A16: (W-min P) `1 = W-bound P by EUCLID:52;

(E-max P) `1 = E-bound P by EUCLID:52;

then q1 in { p where p is Point of (TOP-REAL 2) : p `1 = ((W-bound P) + (E-bound P)) / 2 } by A15, A16;

then P01 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) <> {} by A14, XBOOLE_0:def 4;

then A17: P01 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) ;

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

A18: q2 in P002 and

A19: q2 `1 = (((W-min P) `1) + ((E-max P) `1)) / 2 by A4, Th12;

q2 in { p where p is Point of (TOP-REAL 2) : p `1 = ((W-bound P) + (E-bound P)) / 2 } by A9, A16, A19;

then P02 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) <> {} by A18, XBOOLE_0:def 4;

then A20: P02 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) ;

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) )

assume P is being_simple_closed_curve ; :: thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )

then reconsider P = P as Simple_closed_curve ;

A1: W-min P in P by SPRECT_1:13;

A2: E-max P in P by SPRECT_1:14;

W-min P <> E-max P by TOPREAL5:19;

then consider P01, P02 being non empty Subset of (TOP-REAL 2) such that

A3: P01 is_an_arc_of W-min P, E-max P and

A4: P02 is_an_arc_of W-min P, E-max P and

A5: P = P01 \/ P02 and

A6: P01 /\ P02 = {(W-min P),(E-max P)} by A1, A2, TOPREAL2:5;

reconsider P01 = P01, P02 = P02 as non empty Subset of (TOP-REAL 2) ;

A7: P01 is_an_arc_of E-max P, W-min P by A3, JORDAN5B:14;

A8: P02 is_an_arc_of E-max P, W-min P by A4, JORDAN5B:14;

reconsider P001 = P01, P002 = P02 as non empty Subset of (TOP-REAL 2) ;

A9: (E-max P) `1 = E-bound P by EUCLID:52;

A10: Vertical_Line (((W-bound P) + (E-bound P)) / 2) is closed by Th6;

P01 is closed by A3, COMPTS_1:7, JORDAN5A:1;

then A11: P01 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed by A10, TOPS_1:8;

A12: Vertical_Line (((W-bound P) + (E-bound P)) / 2) is closed by Th6;

P02 is closed by A4, COMPTS_1:7, JORDAN5A:1;

then A13: P02 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed by A12, TOPS_1:8;

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

A14: q1 in P001 and

A15: q1 `1 = (((W-min P) `1) + ((E-max P) `1)) / 2 by A3, Th12;

A16: (W-min P) `1 = W-bound P by EUCLID:52;

(E-max P) `1 = E-bound P by EUCLID:52;

then q1 in { p where p is Point of (TOP-REAL 2) : p `1 = ((W-bound P) + (E-bound P)) / 2 } by A15, A16;

then P01 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) <> {} by A14, XBOOLE_0:def 4;

then A17: P01 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) ;

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

A18: q2 in P002 and

A19: q2 `1 = (((W-min P) `1) + ((E-max P) `1)) / 2 by A4, Th12;

q2 in { p where p is Point of (TOP-REAL 2) : p `1 = ((W-bound P) + (E-bound P)) / 2 } by A9, A16, A19;

then P02 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) <> {} by A18, XBOOLE_0:def 4;

then A20: P02 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) ;

per cases
( (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 or (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 <= (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )
;

end;

suppose
(First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2
; :: thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )

hence
ex P1, P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A3, A5, A6, A8; :: thesis: verum

end;( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A3, A5, A6, A8; :: thesis: verum

suppose A21:
(First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 <= (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2
; :: thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )

A30: P1 is_an_arc_of W-min P, E-max P and

A31: P2 is_an_arc_of E-max P, W-min P and

A32: P1 /\ P2 = {(W-min P),(E-max P)} and

A33: P1 \/ P2 = P and

A34: (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ;

reconsider P1 = P1, P2 = P2 as non empty Subset of (TOP-REAL 2) ;

take P1 ; :: thesis: ex P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )

take P2 ; :: thesis: ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )

thus ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A30, A31, A32, A33, A34; :: thesis: verum

end;

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )

now :: thesis: ( ( (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 < (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 & ex P1, P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) ) or ( (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 = (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 & contradiction ) )end;

then consider P1, P2 being non empty Subset of (TOP-REAL 2) such that ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) ) or ( (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 = (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 & contradiction ) )

per cases
( (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 < (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 or (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 = (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )
by A21, XXREAL_0:1;

end;

case A22:
(First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 < (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2
; :: thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )

A23:
First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = Last_Point (P01,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))
by A3, A11, A17, JORDAN5C:18;

Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = First_Point (P02,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) by A4, A13, A20, JORDAN5C:18;

hence ex P1, P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A4, A5, A6, A7, A22, A23; :: thesis: verum

end;Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = First_Point (P02,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) by A4, A13, A20, JORDAN5C:18;

hence ex P1, P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A4, A5, A6, A7, A22, A23; :: thesis: verum

case A24:
(First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 = (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2
; :: thesis: contradiction

set p = First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)));

set p9 = Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)));

A25: First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P01 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) by A3, A11, A17, JORDAN5C:def 1;

then A26: First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P01 by XBOOLE_0:def 4;

First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in Vertical_Line (((W-bound P) + (E-bound P)) / 2) by A25, XBOOLE_0:def 4;

then A27: (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `1 = ((W-bound P) + (E-bound P)) / 2 by Th31;

A28: Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P02 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) by A8, A13, A20, JORDAN5C:def 2;

then A29: Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P02 by XBOOLE_0:def 4;

Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in Vertical_Line (((W-bound P) + (E-bound P)) / 2) by A28, XBOOLE_0:def 4;

then (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `1 = ((W-bound P) + (E-bound P)) / 2 by Th31;

then First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) by A24, A27, TOPREAL3:6;

then First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P01 /\ P02 by A26, A29, XBOOLE_0:def 4;

then ( First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = W-min P or First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = E-max P ) by A6, TARSKI:def 2;

hence contradiction by A9, A16, A27, TOPREAL5:17; :: thesis: verum

end;set p9 = Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)));

A25: First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P01 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) by A3, A11, A17, JORDAN5C:def 1;

then A26: First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P01 by XBOOLE_0:def 4;

First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in Vertical_Line (((W-bound P) + (E-bound P)) / 2) by A25, XBOOLE_0:def 4;

then A27: (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `1 = ((W-bound P) + (E-bound P)) / 2 by Th31;

A28: Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P02 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) by A8, A13, A20, JORDAN5C:def 2;

then A29: Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P02 by XBOOLE_0:def 4;

Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in Vertical_Line (((W-bound P) + (E-bound P)) / 2) by A28, XBOOLE_0:def 4;

then (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `1 = ((W-bound P) + (E-bound P)) / 2 by Th31;

then First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) by A24, A27, TOPREAL3:6;

then First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P01 /\ P02 by A26, A29, XBOOLE_0:def 4;

then ( First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = W-min P or First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = E-max P ) by A6, TARSKI:def 2;

hence contradiction by A9, A16, A27, TOPREAL5:17; :: thesis: verum

A30: P1 is_an_arc_of W-min P, E-max P and

A31: P2 is_an_arc_of E-max P, W-min P and

A32: P1 /\ P2 = {(W-min P),(E-max P)} and

A33: P1 \/ P2 = P and

A34: (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ;

reconsider P1 = P1, P2 = P2 as non empty Subset of (TOP-REAL 2) ;

take P1 ; :: thesis: ex P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )

take P2 ; :: thesis: ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )

thus ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A30, A31, A32, A33, A34; :: thesis: verum