let C be Simple_closed_curve; :: thesis: for p being Point of (TOP-REAL 2) st p in C & p <> W-min C holds
Segment p,(W-min C),C is_an_arc_of p, W-min C
set q = W-min C;
let p be Point of (TOP-REAL 2); :: thesis: ( p in C & p <> W-min C implies Segment p,(W-min C),C is_an_arc_of p, W-min C )
assume that
A1: p in C and
A2: p <> W-min C ; :: thesis: Segment p,(W-min C),C is_an_arc_of p, W-min C
A3: E-max C in C by SPRECT_1:16;
A4: Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:65;
A5: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:65;
A6: W-min C <> E-max C by TOPREAL5:25;

per cases ( ( p <> E-max C & LE p, E-max C,C ) or p = E-max C or ( p <> E-max C & LE E-max C,p,C ) ) by A1, A3, JORDAN16:11;

suppose that A7: p <> E-max C and
A8: LE p, E-max C,C ; :: thesis: Segment p,(W-min C),C is_an_arc_of p, W-min C

A9: now

assume W-min C in (R_Segment (Upper_Arc C),(W-min C),(E-max C),p) /\ (L_Segment (Lower_Arc C),(E-max C),(W-min C),(W-min C)) ; :: thesis: contradiction
then W-min C in R_Segment (Upper_Arc C),(W-min C),(E-max C),p by XBOOLE_0:def 4;
hence contradiction by A2, A4, JORDAN6:75; :: thesis: verum

end;

p in Upper_Arc C by A8, JORDAN17:3;
then A10: LE p, E-max C, Upper_Arc C, W-min C, E-max C by A4, JORDAN5C:10;
A11: 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) by Th15;
then A12: E-max C in R_Segment (Upper_Arc C),(W-min C),(E-max C),p by A4, A10, JORDAN16:9;
W-min C in Lower_Arc C by JORDAN7:1;
then A13: LE E-max C, W-min C, Lower_Arc C, E-max C, W-min C by A5, JORDAN5C:10;
A14: L_Segment (Lower_Arc C),(E-max C),(W-min C),(W-min C) = Segment (Lower_Arc C),(E-max C),(W-min C),(E-max C),(W-min C) by Th16;
then E-max C in L_Segment (Lower_Arc C),(E-max C),(W-min C),(W-min C) by A5, A13, JORDAN16:9;
then A15: E-max C in (R_Segment (Upper_Arc C),(W-min C),(E-max C),p) /\ (L_Segment (Lower_Arc C),(E-max C),(W-min C),(W-min C)) by A12, XBOOLE_0:def 4;
A16: R_Segment (Upper_Arc C),(W-min C),(E-max C),p c= Upper_Arc C by JORDAN6:21;
A17: L_Segment (Lower_Arc C),(E-max C),(W-min C),(W-min C) c= Lower_Arc C by JORDAN6:20;
(Upper_Arc C) /\ (Lower_Arc C) = {(W-min C),(E-max C)} by JORDAN6:def 9;
then A18: (R_Segment (Upper_Arc C),(W-min C),(E-max C),p) /\ (L_Segment (Lower_Arc C),(E-max C),(W-min C),(W-min C)) = {(E-max C)} by A9, A15, A16, A17, TOPREAL8:1, XBOOLE_1:27;
A19: R_Segment (Upper_Arc C),(W-min C),(E-max C),p is_an_arc_of p, E-max C by A4, A7, A10, A11, JORDAN16:36;
A20: L_Segment (Lower_Arc C),(E-max C),(W-min C),(W-min C) is_an_arc_of E-max C, W-min C by A5, A6, A13, A14, JORDAN16:36;
Segment p,(W-min C),C = (R_Segment (Upper_Arc C),(W-min C),(E-max C),p) \/ (L_Segment (Lower_Arc C),(E-max C),(W-min C),(W-min C)) by A8, Th14;
hence Segment p,(W-min C),C is_an_arc_of p, W-min C by A18, A19, A20, TOPREAL1:5; :: thesis: verum

end;

suppose A21: p = E-max C ; :: thesis: Segment p,(W-min C),C is_an_arc_of p, W-min C

then Segment p,(W-min C),C = Lower_Arc C by JORDAN7:4;
hence Segment p,(W-min C),C is_an_arc_of p, W-min C by A21, JORDAN6:65; :: thesis: verum

end;

suppose that p <> E-max C and
A22: LE E-max C,p,C ; :: thesis: Segment p,(W-min C),C is_an_arc_of p, W-min C

A23: Segment p,(W-min C),C = Segment (Lower_Arc C),(E-max C),(W-min C),p,(W-min C) by A22, Th11;
p in Lower_Arc C by A22, JORDAN17:4;
then LE p, W-min C, Lower_Arc C, E-max C, W-min C by A5, JORDAN5C:10;
hence Segment p,(W-min C),C is_an_arc_of p, W-min C by A2, A5, A23, JORDAN16:36; :: thesis: verum

end;

end;