:: A Decomposition of Simple Closed Curves and an Order of Their Points
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received December 19, 1997
:: Copyright (c) 1997 Association of Mizar Users
theorem :: JORDAN6:1
canceled;
theorem Th2: :: JORDAN6:2
theorem Th3: :: JORDAN6:3
theorem Th4: :: JORDAN6:4
theorem Th5: :: JORDAN6:5
theorem Th6: :: JORDAN6:6
theorem Th7: :: JORDAN6:7
theorem Th8: :: JORDAN6:8
theorem Th9: :: JORDAN6:9
theorem Th10: :: JORDAN6:10
theorem Th11: :: JORDAN6:11
theorem :: JORDAN6:12
theorem Th13: :: JORDAN6:13
theorem Th14: :: JORDAN6:14
theorem Th15: :: JORDAN6:15
definition
let P be
Subset of
(TOP-REAL 2);
let p1,
p2 be
Point of
(TOP-REAL 2);
func x_Middle P,
p1,
p2 -> Point of
(TOP-REAL 2) means :
Def1:
:: JORDAN6:def 1
for
Q being
Subset of
(TOP-REAL 2) st
Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1 ) + (p2 `1 )) / 2 } holds
it = First_Point P,
p1,
p2,
Q;
existence
ex b1 being Point of (TOP-REAL 2) st
for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1 ) + (p2 `1 )) / 2 } holds
b1 = First_Point P,p1,p2,Q
uniqueness
for b1, b2 being Point of (TOP-REAL 2) st ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1 ) + (p2 `1 )) / 2 } holds
b1 = First_Point P,p1,p2,Q ) & ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1 ) + (p2 `1 )) / 2 } holds
b2 = First_Point P,p1,p2,Q ) holds
b1 = b2
end;
:: deftheorem Def1 defines x_Middle JORDAN6:def 1 :
definition
let P be
Subset of
(TOP-REAL 2);
let p1,
p2 be
Point of
(TOP-REAL 2);
func y_Middle P,
p1,
p2 -> Point of
(TOP-REAL 2) means :
Def2:
:: JORDAN6:def 2
for
Q being
Subset of
(TOP-REAL 2) st
Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2 ) + (p2 `2 )) / 2 } holds
it = First_Point P,
p1,
p2,
Q;
existence
ex b1 being Point of (TOP-REAL 2) st
for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2 ) + (p2 `2 )) / 2 } holds
b1 = First_Point P,p1,p2,Q
uniqueness
for b1, b2 being Point of (TOP-REAL 2) st ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2 ) + (p2 `2 )) / 2 } holds
b1 = First_Point P,p1,p2,Q ) & ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2 ) + (p2 `2 )) / 2 } holds
b2 = First_Point P,p1,p2,Q ) holds
b1 = b2
end;
:: deftheorem Def2 defines y_Middle JORDAN6:def 2 :
theorem :: JORDAN6:16
theorem :: JORDAN6:17
theorem :: JORDAN6:18
theorem Th19: :: JORDAN6:19
for
P being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
P is_an_arc_of p1,
p2 &
LE q1,
q2,
P,
p1,
p2 holds
LE q2,
q1,
P,
p2,
p1
definition
let P be
Subset of
(TOP-REAL 2);
let p1,
p2,
q1 be
Point of
(TOP-REAL 2);
func L_Segment P,
p1,
p2,
q1 -> Subset of
(TOP-REAL 2) equals :: JORDAN6:def 3
{ q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } ;
coherence
{ q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } is Subset of (TOP-REAL 2)
end;
:: deftheorem defines L_Segment JORDAN6:def 3 :
definition
let P be
Subset of
(TOP-REAL 2);
let p1,
p2,
q1 be
Point of
(TOP-REAL 2);
func R_Segment P,
p1,
p2,
q1 -> Subset of
(TOP-REAL 2) equals :: JORDAN6:def 4
{ q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ;
coherence
{ q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } is Subset of (TOP-REAL 2)
end;
:: deftheorem defines R_Segment JORDAN6:def 4 :
theorem Th20: :: JORDAN6:20
theorem Th21: :: JORDAN6:21
theorem :: JORDAN6:22
theorem :: JORDAN6:23
canceled;
theorem :: JORDAN6:24
canceled;
theorem :: JORDAN6:25
theorem :: JORDAN6:26
theorem :: JORDAN6:27
theorem :: JORDAN6:28
definition
let P be
Subset of
(TOP-REAL 2);
let p1,
p2,
q1,
q2 be
Point of
(TOP-REAL 2);
func Segment P,
p1,
p2,
q1,
q2 -> Subset of
(TOP-REAL 2) equals :: JORDAN6:def 5
(R_Segment P,p1,p2,q1) /\ (L_Segment P,p1,p2,q2);
correctness
coherence
(R_Segment P,p1,p2,q1) /\ (L_Segment P,p1,p2,q2) is Subset of (TOP-REAL 2);
;
end;
:: deftheorem defines Segment JORDAN6:def 5 :
for
P being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) holds
Segment P,
p1,
p2,
q1,
q2 = (R_Segment P,p1,p2,q1) /\ (L_Segment P,p1,p2,q2);
theorem :: JORDAN6:29
for
P being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) holds
Segment P,
p1,
p2,
q1,
q2 = { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) }
theorem :: JORDAN6:30
for
P being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
P is_an_arc_of p1,
p2 &
LE q2,
q1,
P,
p2,
p1 holds
LE q1,
q2,
P,
p1,
p2 by Th19, JORDAN5B:14;
theorem Th31: :: JORDAN6:31
theorem :: JORDAN6:32
for
P being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
P is_an_arc_of p1,
p2 &
q1 in P &
q2 in P holds
Segment P,
p1,
p2,
q1,
q2 = Segment P,
p2,
p1,
q2,
q1
:: deftheorem defines Vertical_Line JORDAN6:def 6 :
:: deftheorem defines Horizontal_Line JORDAN6:def 7 :
theorem :: JORDAN6:33
theorem Th34: :: JORDAN6:34
theorem :: JORDAN6:35
theorem :: JORDAN6:36
canceled;
theorem :: JORDAN6:37
canceled;
theorem :: JORDAN6:38
canceled;
theorem :: JORDAN6:39
canceled;
theorem Th40: :: JORDAN6:40
for
P being
Subset of
(TOP-REAL 2) st
P is
being_simple_closed_curve holds
ex
P1,
P2 being non
empty Subset of
(TOP-REAL 2) st
(
P1 is_an_arc_of W-min P,
E-max P &
P2 is_an_arc_of E-max P,
W-min P &
P1 /\ P2 = {(W-min P),(E-max P)} &
P1 \/ P2 = P &
(First_Point P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 )
theorem Th41: :: JORDAN6:41
theorem :: JORDAN6:42
canceled;
theorem :: JORDAN6:43
canceled;
theorem :: JORDAN6:44
canceled;
theorem :: JORDAN6:45
canceled;
theorem :: JORDAN6:46
theorem :: JORDAN6:47
canceled;
theorem Th48: :: JORDAN6:48
theorem Th49: :: JORDAN6:49
theorem :: JORDAN6:50
theorem :: JORDAN6:51
canceled;
theorem Th52: :: JORDAN6:52
theorem Th53: :: JORDAN6:53
theorem Th54: :: JORDAN6:54
theorem Th55: :: JORDAN6:55
theorem :: JORDAN6:56
theorem :: JORDAN6:57
theorem Th58: :: JORDAN6:58
theorem Th59: :: JORDAN6:59
theorem Th60: :: JORDAN6:60
theorem Th61: :: JORDAN6:61
Lm1:
for g being Function of I[01] ,R^1
for s1, s2, r being real number st g is continuous & g . 0[01] < r & r < g . 1[01] & s1 = g . 0 & s2 = g . 1 holds
ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = r )
theorem :: JORDAN6:62
canceled;
theorem :: JORDAN6:63
canceled;
theorem Th64: :: JORDAN6:64
Lm2:
now
let P be
Simple_closed_curve;
:: thesis: for P1, P1' being non empty Subset of (TOP-REAL 2) st ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 ) & ex P2' being non empty Subset of (TOP-REAL 2) st
( P1' is_an_arc_of W-min P, E-max P & P2' is_an_arc_of E-max P, W-min P & P1' /\ P2' = {(W-min P),(E-max P)} & P1' \/ P2' = P & (First_Point P1',(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P2',(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 ) holds
P1 = P1'let P1,
P1' be non
empty Subset of
(TOP-REAL 2);
:: thesis: ( ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 ) & ex P2' being non empty Subset of (TOP-REAL 2) st
( P1' is_an_arc_of W-min P, E-max P & P2' is_an_arc_of E-max P, W-min P & P1' /\ P2' = {(W-min P),(E-max P)} & P1' \/ P2' = P & (First_Point P1',(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P2',(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 ) implies P1 = P1' )assume A1:
( ex
P2 being non
empty Subset of
(TOP-REAL 2) st
(
P1 is_an_arc_of W-min P,
E-max P &
P2 is_an_arc_of E-max P,
W-min P &
P1 /\ P2 = {(W-min P),(E-max P)} &
P1 \/ P2 = P &
(First_Point P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 ) & ex
P2' being non
empty Subset of
(TOP-REAL 2) st
(
P1' is_an_arc_of W-min P,
E-max P &
P2' is_an_arc_of E-max P,
W-min P &
P1' /\ P2' = {(W-min P),(E-max P)} &
P1' \/ P2' = P &
(First_Point P1',(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P2',(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 ) )
;
:: thesis: P1 = P1'then consider P2 being non
empty Subset of
(TOP-REAL 2) such that A2:
(
P1 is_an_arc_of W-min P,
E-max P &
P2 is_an_arc_of E-max P,
W-min P &
P1 /\ P2 = {(W-min P),(E-max P)} &
P1 \/ P2 = P &
(First_Point P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 )
;
A3:
P2 is_an_arc_of W-min P,
E-max P
by A2, JORDAN5B:14;
consider P2' being non
empty Subset of
(TOP-REAL 2) such that A4:
(
P1' is_an_arc_of W-min P,
E-max P &
P2' is_an_arc_of E-max P,
W-min P &
P1' /\ P2' = {(W-min P),(E-max P)} &
P1' \/ P2' = P &
(First_Point P1',(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P2',(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 )
by A1;
A5:
P2' is_an_arc_of W-min P,
E-max P
by A4, JORDAN5B:14;
now
assume A6:
(
P1 = P2' &
P2 = P1' )
;
:: thesis: contradictionA7:
(W-min P) `1 = W-bound P
by EUCLID:56;
A8:
(E-max P) `1 = E-bound P
by EUCLID:56;
then
(W-min P) `1 < (E-max P) `1
by A7, TOPREAL5:23;
then A9:
(
(W-min P) `1 <= ((W-bound P) + (E-bound P)) / 2 &
((W-bound P) + (E-bound P)) / 2
<= (E-max P) `1 )
by A7, A8, XREAL_1:228;
then
(
P2 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) &
P2 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is
closed )
by A3, Th64;
then A10:
(First_Point P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (First_Point P2,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2
by A2, JORDAN5C:18;
(
P2' meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) &
P2' /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is
closed )
by A5, A9, Th64;
hence
contradiction
by A4, A6, A10, JORDAN5C:18;
:: thesis: verum
end;
hence
P1 = P1'
by A2, A3, A4, A5, Th61;
:: thesis: verum
end;
definition
let P be
Subset of
(TOP-REAL 2);
assume A1:
P is
being_simple_closed_curve
;
func Upper_Arc P -> non
empty Subset of
(TOP-REAL 2) means :
Def8:
:: JORDAN6:def 8
(
it is_an_arc_of W-min P,
E-max P & ex
P2 being non
empty Subset of
(TOP-REAL 2) st
(
P2 is_an_arc_of E-max P,
W-min P &
it /\ P2 = {(W-min P),(E-max P)} &
it \/ P2 = P &
(First_Point it,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 ) );
existence
ex b1 being non empty Subset of (TOP-REAL 2) st
( b1 is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P & b1 /\ P2 = {(W-min P),(E-max P)} & b1 \/ P2 = P & (First_Point b1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 ) )
uniqueness
for b1, b2 being non empty Subset of (TOP-REAL 2) st b1 is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P & b1 /\ P2 = {(W-min P),(E-max P)} & b1 \/ P2 = P & (First_Point b1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 ) & b2 is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P & b2 /\ P2 = {(W-min P),(E-max P)} & b2 \/ P2 = P & (First_Point b2,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 ) holds
b1 = b2
by A1, Lm2;
end;
:: deftheorem Def8 defines Upper_Arc JORDAN6:def 8 :
definition
let P be
Subset of
(TOP-REAL 2);
assume A1:
P is
being_simple_closed_curve
;
then A2:
Upper_Arc P is_an_arc_of W-min P,
E-max P
by Def8;
func Lower_Arc P -> non
empty Subset of
(TOP-REAL 2) means :
Def9:
:: JORDAN6:def 9
(
it is_an_arc_of E-max P,
W-min P &
(Upper_Arc P) /\ it = {(W-min P),(E-max P)} &
(Upper_Arc P) \/ it = P &
(First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point it,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 );
existence
ex b1 being non empty Subset of (TOP-REAL 2) st
( b1 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b1 = P & (First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point b1,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 )
by A1, Def8;
uniqueness
for b1, b2 being non empty Subset of (TOP-REAL 2) st b1 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b1 = P & (First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point b1,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 & b2 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b2 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b2 = P & (First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point b2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 holds
b1 = b2
end;
:: deftheorem Def9 defines Lower_Arc JORDAN6:def 9 :
theorem Th65: :: JORDAN6:65
for
P being
Subset of
(TOP-REAL 2) st
P is
being_simple_closed_curve holds
(
Upper_Arc P is_an_arc_of W-min P,
E-max P &
Upper_Arc P is_an_arc_of E-max P,
W-min P &
Lower_Arc P is_an_arc_of E-max P,
W-min P &
Lower_Arc P is_an_arc_of W-min P,
E-max P &
(Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} &
(Upper_Arc P) \/ (Lower_Arc P) = P &
(First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point (Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 )
theorem Th66: :: JORDAN6:66
theorem :: JORDAN6:67
theorem :: JORDAN6:68
theorem Th69: :: JORDAN6:69
theorem Th70: :: JORDAN6:70
definition
let P be
Subset of
(TOP-REAL 2);
let q1,
q2 be
Point of
(TOP-REAL 2);
pred LE q1,
q2,
P means :
Def10:
:: JORDAN6:def 10
( (
q1 in Upper_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P ) or (
q1 in Upper_Arc P &
q2 in Upper_Arc P &
LE q1,
q2,
Upper_Arc P,
W-min P,
E-max P ) or (
q1 in Lower_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P &
LE q1,
q2,
Lower_Arc P,
E-max P,
W-min P ) );
end;
:: deftheorem Def10 defines LE JORDAN6:def 10 :
for
P being
Subset of
(TOP-REAL 2) for
q1,
q2 being
Point of
(TOP-REAL 2) holds
(
LE q1,
q2,
P iff ( (
q1 in Upper_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P ) or (
q1 in Upper_Arc P &
q2 in Upper_Arc P &
LE q1,
q2,
Upper_Arc P,
W-min P,
E-max P ) or (
q1 in Lower_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P &
LE q1,
q2,
Lower_Arc P,
E-max P,
W-min P ) ) );
theorem :: JORDAN6:71
theorem :: JORDAN6:72
theorem :: JORDAN6:73
theorem :: JORDAN6:74
theorem :: JORDAN6:75
theorem Th76: :: JORDAN6:76
definition
let C be
Simple_closed_curve;
func Lower_Middle_Point C -> Point of
(TOP-REAL 2) equals :: JORDAN6:def 11
First_Point (Lower_Arc C),
(W-min C),
(E-max C),
(Vertical_Line (((W-bound C) + (E-bound C)) / 2));
coherence
First_Point (Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is Point of (TOP-REAL 2)
;
func Upper_Middle_Point C -> Point of
(TOP-REAL 2) equals :: JORDAN6:def 12
First_Point (Upper_Arc C),
(W-min C),
(E-max C),
(Vertical_Line (((W-bound C) + (E-bound C)) / 2));
coherence
First_Point (Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is Point of (TOP-REAL 2)
;
end;
:: deftheorem defines Lower_Middle_Point JORDAN6:def 11 :
:: deftheorem defines Upper_Middle_Point JORDAN6:def 12 :
theorem Th77: :: JORDAN6:77
theorem Th78: :: JORDAN6:78
theorem :: JORDAN6:79
theorem :: JORDAN6:80
theorem :: JORDAN6:81
theorem Th82: :: JORDAN6:82
theorem :: JORDAN6:83
theorem :: JORDAN6:84
theorem :: JORDAN6:85