let P be Subset of (); :: thesis: ( P is being_simple_closed_curve implies ex P1, P2 being non empty Subset of () 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 = {(),()} & P1 \/ P2 = P & (First_Point (P1,(),(),(Vertical_Line ((() + ()) / 2)))) `2 > (Last_Point (P2,(),(),(Vertical_Line ((() + ()) / 2)))) `2 ) )

assume P is being_simple_closed_curve ; :: thesis: ex P1, P2 being non empty Subset of () 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 = {(),()} & P1 \/ P2 = P & (First_Point (P1,(),(),(Vertical_Line ((() + ()) / 2)))) `2 > (Last_Point (P2,(),(),(Vertical_Line ((() + ()) / 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 () 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 = {(),()} by ;
reconsider P01 = P01, P02 = P02 as non empty Subset of () ;
A7: P01 is_an_arc_of E-max P, W-min P by ;
A8: P02 is_an_arc_of E-max P, W-min P by ;
reconsider P001 = P01, P002 = P02 as non empty Subset of () ;
A9: (E-max P) `1 = E-bound P by EUCLID:52;
A10: Vertical_Line ((() + ()) / 2) is closed by Th6;
P01 is closed by ;
then A11: P01 /\ (Vertical_Line ((() + ()) / 2)) is closed by ;
A12: Vertical_Line ((() + ()) / 2) is closed by Th6;
P02 is closed by ;
then A13: P02 /\ (Vertical_Line ((() + ()) / 2)) is closed by ;
consider q1 being Point of () such that
A14: q1 in P001 and
A15: q1 `1 = ((() `1) + (() `1)) / 2 by ;
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 () : p `1 = (() + ()) / 2 } by ;
then P01 /\ (Vertical_Line ((() + ()) / 2)) <> {} by ;
then A17: P01 meets Vertical_Line ((() + ()) / 2) ;
consider q2 being Point of () such that
A18: q2 in P002 and
A19: q2 `1 = ((() `1) + (() `1)) / 2 by ;
q2 in { p where p is Point of () : p `1 = (() + ()) / 2 } by A9, A16, A19;
then P02 /\ (Vertical_Line ((() + ()) / 2)) <> {} by ;
then A20: P02 meets Vertical_Line ((() + ()) / 2) ;
per cases ( (First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2)))) `2 > (Last_Point (P02,(),(),(Vertical_Line ((() + ()) / 2)))) `2 or (First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2)))) `2 <= (Last_Point (P02,(),(),(Vertical_Line ((() + ()) / 2)))) `2 ) ;
suppose (First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2)))) `2 > (Last_Point (P02,(),(),(Vertical_Line ((() + ()) / 2)))) `2 ; :: thesis: ex P1, P2 being non empty Subset of () 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 = {(),()} & P1 \/ P2 = P & (First_Point (P1,(),(),(Vertical_Line ((() + ()) / 2)))) `2 > (Last_Point (P2,(),(),(Vertical_Line ((() + ()) / 2)))) `2 )

hence ex P1, P2 being non empty Subset of () 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 = {(),()} & P1 \/ P2 = P & (First_Point (P1,(),(),(Vertical_Line ((() + ()) / 2)))) `2 > (Last_Point (P2,(),(),(Vertical_Line ((() + ()) / 2)))) `2 ) by A3, A5, A6, A8; :: thesis: verum
end;
suppose A21: (First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2)))) `2 <= (Last_Point (P02,(),(),(Vertical_Line ((() + ()) / 2)))) `2 ; :: thesis: ex P1, P2 being non empty Subset of () 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 = {(),()} & P1 \/ P2 = P & (First_Point (P1,(),(),(Vertical_Line ((() + ()) / 2)))) `2 > (Last_Point (P2,(),(),(Vertical_Line ((() + ()) / 2)))) `2 )

now :: thesis: ( ( (First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2)))) `2 < (Last_Point (P02,(),(),(Vertical_Line ((() + ()) / 2)))) `2 & ex P1, P2 being non empty Subset of () 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 = {(),()} & P1 \/ P2 = P & (First_Point (P1,(),(),(Vertical_Line ((() + ()) / 2)))) `2 > (Last_Point (P2,(),(),(Vertical_Line ((() + ()) / 2)))) `2 ) ) or ( (First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2)))) `2 = (Last_Point (P02,(),(),(Vertical_Line ((() + ()) / 2)))) `2 & contradiction ) )
per cases ( (First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2)))) `2 < (Last_Point (P02,(),(),(Vertical_Line ((() + ()) / 2)))) `2 or (First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2)))) `2 = (Last_Point (P02,(),(),(Vertical_Line ((() + ()) / 2)))) `2 ) by ;
case A22: (First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2)))) `2 < (Last_Point (P02,(),(),(Vertical_Line ((() + ()) / 2)))) `2 ; :: thesis: ex P1, P2 being non empty Subset of () 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 = {(),()} & P1 \/ P2 = P & (First_Point (P1,(),(),(Vertical_Line ((() + ()) / 2)))) `2 > (Last_Point (P2,(),(),(Vertical_Line ((() + ()) / 2)))) `2 )

A23: First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2))) = Last_Point (P01,(),(),(Vertical_Line ((() + ()) / 2))) by ;
Last_Point (P02,(),(),(Vertical_Line ((() + ()) / 2))) = First_Point (P02,(),(),(Vertical_Line ((() + ()) / 2))) by ;
hence ex P1, P2 being non empty Subset of () 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 = {(),()} & P1 \/ P2 = P & (First_Point (P1,(),(),(Vertical_Line ((() + ()) / 2)))) `2 > (Last_Point (P2,(),(),(Vertical_Line ((() + ()) / 2)))) `2 ) by A4, A5, A6, A7, A22, A23; :: thesis: verum
end;
case A24: (First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2)))) `2 = (Last_Point (P02,(),(),(Vertical_Line ((() + ()) / 2)))) `2 ; :: thesis: contradiction
set p = First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2)));
set p9 = Last_Point (P02,(),(),(Vertical_Line ((() + ()) / 2)));
A25: First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2))) in P01 /\ (Vertical_Line ((() + ()) / 2)) by ;
then A26: First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2))) in P01 by XBOOLE_0:def 4;
First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2))) in Vertical_Line ((() + ()) / 2) by ;
then A27: (First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2)))) `1 = (() + ()) / 2 by Th31;
A28: Last_Point (P02,(),(),(Vertical_Line ((() + ()) / 2))) in P02 /\ (Vertical_Line ((() + ()) / 2)) by ;
then A29: Last_Point (P02,(),(),(Vertical_Line ((() + ()) / 2))) in P02 by XBOOLE_0:def 4;
Last_Point (P02,(),(),(Vertical_Line ((() + ()) / 2))) in Vertical_Line ((() + ()) / 2) by ;
then (Last_Point (P02,(),(),(Vertical_Line ((() + ()) / 2)))) `1 = (() + ()) / 2 by Th31;
then First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2))) = Last_Point (P02,(),(),(Vertical_Line ((() + ()) / 2))) by ;
then First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2))) in P01 /\ P02 by ;
then ( First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2))) = W-min P or First_Point (P01,(),(),(Vertical_Line ((() + ()) / 2))) = E-max P ) by ;
hence contradiction by A9, A16, A27, TOPREAL5:17; :: thesis: verum
end;
end;
end;
then consider P1, P2 being non empty Subset of () such that
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 = {(),()} and
A33: P1 \/ P2 = P and
A34: (First_Point (P1,(),(),(Vertical_Line ((() + ()) / 2)))) `2 > (Last_Point (P2,(),(),(Vertical_Line ((() + ()) / 2)))) `2 ;
reconsider P1 = P1, P2 = P2 as non empty Subset of () ;
take P1 ; :: thesis: ex P2 being non empty Subset of () 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 = {(),()} & P1 \/ P2 = P & (First_Point (P1,(),(),(Vertical_Line ((() + ()) / 2)))) `2 > (Last_Point (P2,(),(),(Vertical_Line ((() + ()) / 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 = {(),()} & P1 \/ P2 = P & (First_Point (P1,(),(),(Vertical_Line ((() + ()) / 2)))) `2 > (Last_Point (P2,(),(),(Vertical_Line ((() + ()) / 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 = {(),()} & P1 \/ P2 = P & (First_Point (P1,(),(),(Vertical_Line ((() + ()) / 2)))) `2 > (Last_Point (P2,(),(),(Vertical_Line ((() + ()) / 2)))) `2 ) by A30, A31, A32, A33, A34; :: thesis: verum
end;
end;