ex P1, P2 being non empty Subset of (TOP-REAL 2) st

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

hence ex b_{1} being non empty Subset of (TOP-REAL 2) st

( b_{1} 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_{1} /\ P2 = {(W-min P),(E-max P)} & b_{1} \/ P2 = P & (First_Point (b_{1},(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 ) )
; :: thesis: verum

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

hence ex b

( b

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