let P1, P1' be non empty Subset of (TOP-REAL 2); :: thesis: ( P1 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P1 = P & (First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P1,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 & P1' is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ P1' = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P1' = P & (First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P1',(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 implies P1 = P1' )
assume that
A3: P1 is_an_arc_of E-max P, W-min P and
(Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} and
A4: (Upper_Arc P) \/ P1 = P and
(First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P1,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 and
A5: P1' is_an_arc_of E-max P, W-min P and
(Upper_Arc P) /\ P1' = {(W-min P),(E-max P)} and
A6: (Upper_Arc P) \/ P1' = P and
(First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P1',(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 ; :: thesis: P1 = P1'
A7: P1 is_an_arc_of W-min P, E-max P by A3, JORDAN5B:14;
P1' is_an_arc_of W-min P, E-max P by A5, JORDAN5B:14;
then ( P1 = P1' or ( Upper_Arc P = P1' & P1 = Upper_Arc P ) ) by A1, A2, A4, A6, A7, Th61;
hence P1 = P1' ; :: thesis: verum