let P be Subset of (TOP-REAL 2); ( 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 & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) )
assume A1:
P is being_simple_closed_curve
; ( 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 & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 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 A1, Def9;
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 & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )
by A1, A2, Def9, JORDAN5B:14; verum