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:65;
then L_Segment (Upper_Arc C),(W-min C),(E-max C),(E-max C) = Upper_Arc C by JORDAN6:25;
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:21, XBOOLE_1:28 ;
:: thesis: verum