let C be Simple_closed_curve; for p, q being Point of (TOP-REAL 2) st p <> q & LE p,q,C holds
Segment (p,q,C) is_an_arc_of p,q
let p, q be Point of (TOP-REAL 2); ( p <> q & LE p,q,C implies Segment (p,q,C) is_an_arc_of p,q )
assume that
A1:
p <> q
and
A2:
LE p,q,C
; Segment (p,q,C) is_an_arc_of p,q
A3:
E-max C in C
by SPRECT_1:14;
A4:
p in C
by A2, JORDAN7:5;
A5:
q in C
by A2, JORDAN7:5;
A6:
Upper_Arc C is_an_arc_of W-min C, E-max C
by JORDAN6:50;
A7:
Lower_Arc C is_an_arc_of E-max C, W-min C
by JORDAN6:50;
per cases
( q = W-min C or ( LE q, E-max C,C & not LE E-max C,q,C & q <> W-min C ) or ( p <> E-max C & LE p, E-max C,C & LE E-max C,q,C & q <> E-max C ) or ( q = E-max C & LE p, E-max C,C & LE E-max C,q,C ) or ( p = E-max C & LE p, E-max C,C & LE E-max C,q,C ) or ( LE E-max C,p,C & not LE p, E-max C,C ) )
by A3, A4, A5, JORDAN16:7;
suppose that A8:
LE q,
E-max C,
C
and A9:
not
LE E-max C,
q,
C
and A10:
q <> W-min C
;
Segment (p,q,C) is_an_arc_of p,qA11:
Segment (
p,
q,
C)
= Segment (
(Upper_Arc C),
(W-min C),
(E-max C),
p,
q)
by A1, A2, A8, Th8;
not
q in Lower_Arc C
by A9, A10, Th5;
then
LE p,
q,
Upper_Arc C,
W-min C,
E-max C
by A2, JORDAN6:def 10;
hence
Segment (
p,
q,
C)
is_an_arc_of p,
q
by A1, A6, A11, JORDAN16:21;
verum end; suppose that A12:
p <> E-max C
and A13:
LE p,
E-max C,
C
and A14:
LE E-max C,
q,
C
and A15:
q <> E-max C
;
Segment (p,q,C) is_an_arc_of p,qA16:
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),q))assume A17:
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),q))
;
contradictionthen
W-min C in R_Segment (
(Upper_Arc C),
(W-min C),
(E-max C),
p)
by XBOOLE_0:def 4;
then A18:
p = W-min C
by A6, JORDAN6:60;
W-min C in L_Segment (
(Lower_Arc C),
(E-max C),
(W-min C),
q)
by A17, XBOOLE_0:def 4;
hence
contradiction
by A1, A7, A18, JORDAN6:59;
verum end;
p in Upper_Arc C
by A13, JORDAN17:3;
then A19:
LE p,
E-max C,
Upper_Arc C,
W-min C,
E-max C
by A6, JORDAN5C:10;
A20:
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 A21:
E-max C in R_Segment (
(Upper_Arc C),
(W-min C),
(E-max C),
p)
by A19, JORDAN16:5;
q in Lower_Arc C
by A14, JORDAN17:4;
then A22:
LE E-max C,
q,
Lower_Arc C,
E-max C,
W-min C
by A7, JORDAN5C:10;
A23:
L_Segment (
(Lower_Arc C),
(E-max C),
(W-min C),
q)
= Segment (
(Lower_Arc C),
(E-max C),
(W-min C),
(E-max C),
q)
by Th15;
then
E-max C in L_Segment (
(Lower_Arc C),
(E-max C),
(W-min C),
q)
by A22, JORDAN16:5;
then A24:
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),q))
by A21, XBOOLE_0:def 4;
A25:
R_Segment (
(Upper_Arc C),
(W-min C),
(E-max C),
p)
c= Upper_Arc C
by JORDAN6:20;
A26:
L_Segment (
(Lower_Arc C),
(E-max C),
(W-min C),
q)
c= Lower_Arc C
by JORDAN6:19;
(Upper_Arc C) /\ (Lower_Arc C) = {(W-min C),(E-max C)}
by JORDAN6:def 9;
then A27:
(R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) = {(E-max C)}
by A16, A24, A25, A26, TOPREAL8:1, XBOOLE_1:27;
A28:
R_Segment (
(Upper_Arc C),
(W-min C),
(E-max C),
p)
is_an_arc_of p,
E-max C
by A6, A12, A19, A20, JORDAN16:21;
A29:
L_Segment (
(Lower_Arc C),
(E-max C),
(W-min C),
q)
is_an_arc_of E-max C,
q
by A7, A15, A22, A23, JORDAN16:21;
Segment (
p,
q,
C)
= (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q))
by A13, A14, Th12;
hence
Segment (
p,
q,
C)
is_an_arc_of p,
q
by A27, A28, A29, TOPREAL1:2;
verum suppose that A30:
q = E-max C
and A31:
LE p,
E-max C,
C
and A32:
LE E-max C,
q,
C
;
Segment (p,q,C) is_an_arc_of p,q
p in Upper_Arc C
by A31, JORDAN17:3;
then A33:
LE p,
E-max C,
Upper_Arc C,
W-min C,
E-max C
by A6, JORDAN5C:10;
A34:
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 A35:
E-max C in R_Segment (
(Upper_Arc C),
(W-min C),
(E-max C),
p)
by A33, JORDAN16:5;
A36:
L_Segment (
(Lower_Arc C),
(E-max C),
(W-min C),
q)
= {(E-max C)}
by A7, A30, JORDAN6:21;
Segment (
p,
q,
C) =
(R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q))
by A31, A32, Th12
.=
R_Segment (
(Upper_Arc C),
(W-min C),
(E-max C),
p)
by A35, A36, ZFMISC_1:40
;
hence
Segment (
p,
q,
C)
is_an_arc_of p,
q
by A1, A6, A30, A33, A34, JORDAN16:21;
verum end; suppose that A37:
p = E-max C
and A38:
LE p,
E-max C,
C
and A39:
LE E-max C,
q,
C
;
Segment (p,q,C) is_an_arc_of p,q
q in Lower_Arc C
by A39, JORDAN17:4;
then A40:
LE E-max C,
q,
Lower_Arc C,
E-max C,
W-min C
by A7, JORDAN5C:10;
A41:
L_Segment (
(Lower_Arc C),
(E-max C),
(W-min C),
q)
= Segment (
(Lower_Arc C),
(E-max C),
(W-min C),
(E-max C),
q)
by Th15;
then A42:
E-max C in L_Segment (
(Lower_Arc C),
(E-max C),
(W-min C),
q)
by A40, JORDAN16:5;
A43:
R_Segment (
(Upper_Arc C),
(W-min C),
(E-max C),
p)
= {(E-max C)}
by A6, A37, JORDAN6:23;
Segment (
p,
q,
C) =
(R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q))
by A38, A39, Th12
.=
L_Segment (
(Lower_Arc C),
(E-max C),
(W-min C),
q)
by A42, A43, ZFMISC_1:40
;
hence
Segment (
p,
q,
C)
is_an_arc_of p,
q
by A1, A7, A37, A40, A41, JORDAN16:21;
verum end; suppose that A44:
LE E-max C,
p,
C
and A45:
not
LE p,
E-max C,
C
;
Segment (p,q,C) is_an_arc_of p,qA46:
Segment (
p,
q,
C)
= Segment (
(Lower_Arc C),
(E-max C),
(W-min C),
p,
q)
by A2, A44, Th11;
not
p in Upper_Arc C
by A45, Th6;
then
LE p,
q,
Lower_Arc C,
E-max C,
W-min C
by A2, JORDAN6:def 10;
hence
Segment (
p,
q,
C)
is_an_arc_of p,
q
by A1, A7, A46, JORDAN16:21;
verum end;