let P be Subset of (); :: thesis: ( P is being_simple_closed_curve implies ( Upper_Arc P is_an_arc_of W-min P, E-max P & Upper_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of W-min P, E-max P & () /\ () = {(),()} & () \/ () = P & (First_Point ((),(),(),(Vertical_Line ((() + ()) / 2)))) `2 > (Last_Point ((),(),(),(Vertical_Line ((() + ()) / 2)))) `2 ) )
assume A1: P is being_simple_closed_curve ; :: thesis: ( Upper_Arc P is_an_arc_of W-min P, E-max P & Upper_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of W-min P, E-max P & () /\ () = {(),()} & () \/ () = P & (First_Point ((),(),(),(Vertical_Line ((() + ()) / 2)))) `2 > (Last_Point ((),(),(),(Vertical_Line ((() + ()) / 2)))) `2 )
then A2: Upper_Arc P is_an_arc_of W-min P, E-max P by Def8;
Lower_Arc P is_an_arc_of E-max P, W-min P by ;
hence ( Upper_Arc P is_an_arc_of W-min P, E-max P & Upper_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of W-min P, E-max P & () /\ () = {(),()} & () \/ () = P & (First_Point ((),(),(),(Vertical_Line ((() + ()) / 2)))) `2 > (Last_Point ((),(),(),(Vertical_Line ((() + ()) / 2)))) `2 ) by ; :: thesis: verum