:: 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₂ being non empty Subset of (TOP-REAL 2) holds
( b₂ = Upper_Arc P iff ( b₂ 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₂ /\ P2 = {(W-min P),(E-max P)} & b₂ \/ P2 = P & (First_Point (b₂,(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 ) ) );