let C be Simple_closed_curve; 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); ( 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
; 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
;
Segment (p,(W-min C),C) is_an_arc_of p, W-min CA9:
now 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)))
;
contradictionthen
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;
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;
verum end; suppose that
p <> E-max C
and A22:
LE E-max C,
p,
C
;
Segment (p,(W-min C),C) is_an_arc_of p, W-min CA23:
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;
verum end; end;