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