:: deftheorem Def8 defines Upper_Arc JORDAN6:def 8 :

for P being Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds

for b_{2} being non empty Subset of (TOP-REAL 2) holds

( b_{2} = Upper_Arc P iff ( b_{2} is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st

( P2 is_an_arc_of E-max P, W-min P & b_{2} /\ P2 = {(W-min P),(E-max P)} & b_{2} \/ P2 = P & (First_Point (b_{2},(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 ) ) );

for P being Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds

for b

( b

( P2 is_an_arc_of E-max P, W-min P & b