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