:: deftheorem Def9 defines Lower_Arc JORDAN6:def 9 :
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₂ = Lower_Arc P iff ( b₂ is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b₂ = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b₂ = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b<sub>2</sub>,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) );