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

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

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

then L_Segment ((Upper_Arc C),(W-min C),(E-max C),(E-max C)) = Upper_Arc C by JORDAN6:22;

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

.= R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) by JORDAN6:20, XBOOLE_1:28 ;

:: thesis: verum

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

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

then L_Segment ((Upper_Arc C),(W-min C),(E-max C),(E-max C)) = Upper_Arc C by JORDAN6:22;

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

.= R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) by JORDAN6:20, XBOOLE_1:28 ;

:: thesis: verum