let C be Simple_closed_curve; :: thesis: for p being Point of (TOP-REAL 2) holds L_Segment ((Lower_Arc C),(E-max C),(W-min C),p) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),p)

let p be Point of (TOP-REAL 2); :: thesis: L_Segment ((Lower_Arc C),(E-max C),(W-min C),p) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),p)

Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;

then R_Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C)) = Lower_Arc C by JORDAN6:24;

hence Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),p) = (Lower_Arc C) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),p)) by JORDAN6:def 5

.= L_Segment ((Lower_Arc C),(E-max C),(W-min C),p) by JORDAN6:19, XBOOLE_1:28 ;

:: thesis: verum

let p be Point of (TOP-REAL 2); :: thesis: L_Segment ((Lower_Arc C),(E-max C),(W-min C),p) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),p)

Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;

then R_Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C)) = Lower_Arc C by JORDAN6:24;

hence Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),p) = (Lower_Arc C) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),p)) by JORDAN6:def 5

.= L_Segment ((Lower_Arc C),(E-max C),(W-min C),p) by JORDAN6:19, XBOOLE_1:28 ;

:: thesis: verum