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:14;
A4: Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50;
A5: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
A6: W-min C <> E-max C by TOPREAL5:19;
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:7;
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 :: thesis: not 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)))
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:60; :: 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 Th14;
then A12: E-max C in R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) by A10, JORDAN16:5;
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 Th15;
then E-max C in L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)) by A13, JORDAN16:5;
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:20;
A17: L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)) c= Lower_Arc C by JORDAN6:19;
(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:21;
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:21;
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, Th13;
hence Segment (p,(W-min C),C) is_an_arc_of p, W-min C by A18, A19, A20, TOPREAL1:2; :: 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:50; :: 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, Th10;
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:21; :: thesis: verum
end;
end;