:: by Robert Milewski

::

:: Received September 27, 2003

:: Copyright (c) 2003-2016 Association of Mizar Users

definition

let C be Simple_closed_curve;

ex b_{1} being SetSequence of the carrier of (TOP-REAL 2) st

for i being Nat holds b_{1} . i = Upper_Arc (L~ (Cage (C,i)))

for b_{1}, b_{2} being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Nat holds b_{1} . i = Upper_Arc (L~ (Cage (C,i))) ) & ( for i being Nat holds b_{2} . i = Upper_Arc (L~ (Cage (C,i))) ) holds

b_{1} = b_{2}

ex b_{1} being SetSequence of the carrier of (TOP-REAL 2) st

for i being Nat holds b_{1} . i = Lower_Arc (L~ (Cage (C,i)))

for b_{1}, b_{2} being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Nat holds b_{1} . i = Lower_Arc (L~ (Cage (C,i))) ) & ( for i being Nat holds b_{2} . i = Lower_Arc (L~ (Cage (C,i))) ) holds

b_{1} = b_{2}

end;
func Upper_Appr C -> SetSequence of the carrier of (TOP-REAL 2) means :Def1: :: JORDAN19:def 1

for i being Nat holds it . i = Upper_Arc (L~ (Cage (C,i)));

existence for i being Nat holds it . i = Upper_Arc (L~ (Cage (C,i)));

ex b

for i being Nat holds b

proof end;

uniqueness for b

b

proof end;

func Lower_Appr C -> SetSequence of the carrier of (TOP-REAL 2) means :Def2: :: JORDAN19:def 2

for i being Nat holds it . i = Lower_Arc (L~ (Cage (C,i)));

existence for i being Nat holds it . i = Lower_Arc (L~ (Cage (C,i)));

ex b

for i being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines Upper_Appr JORDAN19:def 1 :

for C being Simple_closed_curve

for b_{2} being SetSequence of the carrier of (TOP-REAL 2) holds

( b_{2} = Upper_Appr C iff for i being Nat holds b_{2} . i = Upper_Arc (L~ (Cage (C,i))) );

for C being Simple_closed_curve

for b

( b

:: deftheorem Def2 defines Lower_Appr JORDAN19:def 2 :

for C being Simple_closed_curve

for b_{2} being SetSequence of the carrier of (TOP-REAL 2) holds

( b_{2} = Lower_Appr C iff for i being Nat holds b_{2} . i = Lower_Arc (L~ (Cage (C,i))) );

for C being Simple_closed_curve

for b

( b

definition

let C be Simple_closed_curve;

coherence

Lim_inf (Upper_Appr C) is Subset of (TOP-REAL 2) ;

coherence

Lim_inf (Lower_Appr C) is Subset of (TOP-REAL 2) ;

end;
coherence

Lim_inf (Upper_Appr C) is Subset of (TOP-REAL 2) ;

coherence

Lim_inf (Lower_Appr C) is Subset of (TOP-REAL 2) ;

:: deftheorem defines North_Arc JORDAN19:def 3 :

for C being Simple_closed_curve holds North_Arc C = Lim_inf (Upper_Appr C);

for C being Simple_closed_curve holds North_Arc C = Lim_inf (Upper_Appr C);

:: deftheorem defines South_Arc JORDAN19:def 4 :

for C being Simple_closed_curve holds South_Arc C = Lim_inf (Lower_Appr C);

for C being Simple_closed_curve holds South_Arc C = Lim_inf (Lower_Appr C);

Lm1: now :: thesis: for G being Go-board

for j being Nat st 1 <= j & j <= width G holds

[(Center G),j] in Indices G

for j being Nat st 1 <= j & j <= width G holds

[(Center G),j] in Indices G

let G be Go-board; :: thesis: for j being Nat st 1 <= j & j <= width G holds

[(Center G),j] in Indices G

let j be Nat; :: thesis: ( 1 <= j & j <= width G implies [(Center G),j] in Indices G )

assume that

A1: 1 <= j and

A2: j <= width G ; :: thesis: [(Center G),j] in Indices G

0 + 1 <= ((len G) div 2) + 1 by XREAL_1:6;

then A3: 0 + 1 <= Center G by JORDAN1A:def 1;

Center G <= len G by JORDAN1B:13;

hence [(Center G),j] in Indices G by A1, A2, A3, MATRIX_0:30; :: thesis: verum

end;
[(Center G),j] in Indices G

let j be Nat; :: thesis: ( 1 <= j & j <= width G implies [(Center G),j] in Indices G )

assume that

A1: 1 <= j and

A2: j <= width G ; :: thesis: [(Center G),j] in Indices G

0 + 1 <= ((len G) div 2) + 1 by XREAL_1:6;

then A3: 0 + 1 <= Center G by JORDAN1A:def 1;

Center G <= len G by JORDAN1B:13;

hence [(Center G),j] in Indices G by A1, A2, A3, MATRIX_0:30; :: thesis: verum

Lm2: now :: thesis: for D being non empty Subset of (TOP-REAL 2)

for n, i being Nat st [i,(width (Gauge (D,n)))] in Indices (Gauge (D,n)) holds

((Gauge (D,n)) * (i,(width (Gauge (D,n))))) `2 = (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge (D,n))) - 2))

for n, i being Nat st [i,(width (Gauge (D,n)))] in Indices (Gauge (D,n)) holds

((Gauge (D,n)) * (i,(width (Gauge (D,n))))) `2 = (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge (D,n))) - 2))

let D be non empty Subset of (TOP-REAL 2); :: thesis: for n, i being Nat st [i,(width (Gauge (D,n)))] in Indices (Gauge (D,n)) holds

((Gauge (D,n)) * (i,(width (Gauge (D,n))))) `2 = (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge (D,n))) - 2))

let n, i be Nat; :: thesis: ( [i,(width (Gauge (D,n)))] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * (i,(width (Gauge (D,n))))) `2 = (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge (D,n))) - 2)) )

set a = N-bound D;

set s = S-bound D;

set w = W-bound D;

set e = E-bound D;

set G = Gauge (D,n);

assume [i,(width (Gauge (D,n)))] in Indices (Gauge (D,n)) ; :: thesis: ((Gauge (D,n)) * (i,(width (Gauge (D,n))))) `2 = (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge (D,n))) - 2))

hence ((Gauge (D,n)) * (i,(width (Gauge (D,n))))) `2 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (i - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge (D,n))) - 2)))]| `2 by JORDAN8:def 1

.= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge (D,n))) - 2)) by EUCLID:52 ;

:: thesis: verum

end;
((Gauge (D,n)) * (i,(width (Gauge (D,n))))) `2 = (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge (D,n))) - 2))

let n, i be Nat; :: thesis: ( [i,(width (Gauge (D,n)))] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * (i,(width (Gauge (D,n))))) `2 = (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge (D,n))) - 2)) )

set a = N-bound D;

set s = S-bound D;

set w = W-bound D;

set e = E-bound D;

set G = Gauge (D,n);

assume [i,(width (Gauge (D,n)))] in Indices (Gauge (D,n)) ; :: thesis: ((Gauge (D,n)) * (i,(width (Gauge (D,n))))) `2 = (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge (D,n))) - 2))

hence ((Gauge (D,n)) * (i,(width (Gauge (D,n))))) `2 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (i - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge (D,n))) - 2)))]| `2 by JORDAN8:def 1

.= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge (D,n))) - 2)) by EUCLID:52 ;

:: thesis: verum

theorem Th2: :: JORDAN19:2

for n being Nat

for E being compact non horizontal non vertical Subset of (TOP-REAL 2)

for m, j being Nat st 1 <= m & m <= n & 1 <= j & j <= width (Gauge (E,n)) holds

LSeg (((Gauge (E,n)) * ((Center (Gauge (E,n))),(width (Gauge (E,n))))),((Gauge (E,n)) * ((Center (Gauge (E,n))),j))) c= LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),(width (Gauge (E,m))))),((Gauge (E,n)) * ((Center (Gauge (E,n))),j)))

for E being compact non horizontal non vertical Subset of (TOP-REAL 2)

for m, j being Nat st 1 <= m & m <= n & 1 <= j & j <= width (Gauge (E,n)) holds

LSeg (((Gauge (E,n)) * ((Center (Gauge (E,n))),(width (Gauge (E,n))))),((Gauge (E,n)) * ((Center (Gauge (E,n))),j))) c= LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),(width (Gauge (E,m))))),((Gauge (E,n)) * ((Center (Gauge (E,n))),j)))

proof end;

theorem Th3: :: JORDAN19:3

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for i, j being Nat st 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Cage (C,n)) holds

LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets L~ (Upper_Seq (C,n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for i, j being Nat st 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Cage (C,n)) holds

LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets L~ (Upper_Seq (C,n))

proof end;

theorem Th4: :: JORDAN19:4

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for n being Nat st n > 0 holds

for i, j being Nat st 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Cage (C,n)) holds

LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets Upper_Arc (L~ (Cage (C,n)))

for n being Nat st n > 0 holds

for i, j being Nat st 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Cage (C,n)) holds

LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets Upper_Arc (L~ (Cage (C,n)))

proof end;

theorem :: JORDAN19:5

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for j being Nat st (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Lower_Arc (L~ (Cage (C,(n + 1)))) & 1 <= j & j <= width (Gauge (C,(n + 1))) holds

LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))) meets Upper_Arc (L~ (Cage (C,(n + 1))))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for j being Nat st (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Lower_Arc (L~ (Cage (C,(n + 1)))) & 1 <= j & j <= width (Gauge (C,(n + 1))) holds

LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))) meets Upper_Arc (L~ (Cage (C,(n + 1))))

proof end;

theorem Th6: :: JORDAN19:6

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for f being FinSequence of (TOP-REAL 2)

for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on Gauge (C,n) & not dist ((f /. k),(f /. (k + 1))) = ((N-bound C) - (S-bound C)) / (2 |^ n) holds

dist ((f /. k),(f /. (k + 1))) = ((E-bound C) - (W-bound C)) / (2 |^ n)

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for f being FinSequence of (TOP-REAL 2)

for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on Gauge (C,n) & not dist ((f /. k),(f /. (k + 1))) = ((N-bound C) - (S-bound C)) / (2 |^ n) holds

dist ((f /. k),(f /. (k + 1))) = ((E-bound C) - (W-bound C)) / (2 |^ n)

proof end;

theorem :: JORDAN19:7

for M being symmetric triangle MetrStruct

for r being Real

for p, q, x being Element of M st p in Ball (x,r) & q in Ball (x,r) holds

dist (p,q) < 2 * r

for r being Real

for p, q, x being Element of M st p in Ball (x,r) & q in Ball (x,r) holds

dist (p,q) < 2 * r

proof end;

theorem :: JORDAN19:8

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-bound C < N-bound (L~ (Cage (C,n)))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-bound C < N-bound (L~ (Cage (C,n)))

proof end;

theorem Th9: :: JORDAN19:9

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds E-bound C < E-bound (L~ (Cage (C,n)))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds E-bound C < E-bound (L~ (Cage (C,n)))

proof end;

theorem :: JORDAN19:10

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds S-bound (L~ (Cage (C,n))) < S-bound C

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds S-bound (L~ (Cage (C,n))) < S-bound C

proof end;

theorem Th11: :: JORDAN19:11

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds W-bound (L~ (Cage (C,n))) < W-bound C

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds W-bound (L~ (Cage (C,n))) < W-bound C

proof end;

theorem Th12: :: JORDAN19:12

for n being Nat

for C being Simple_closed_curve

for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= k & k <= j & j <= width (Gauge (C,n)) & (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j))} holds

LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))) meets Upper_Arc C

for C being Simple_closed_curve

for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= k & k <= j & j <= width (Gauge (C,n)) & (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j))} holds

LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))) meets Upper_Arc C

proof end;

theorem Th13: :: JORDAN19:13

for n being Nat

for C being Simple_closed_curve

for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= k & k <= j & j <= width (Gauge (C,n)) & (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j))} holds

LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))) meets Lower_Arc C

for C being Simple_closed_curve

for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= k & k <= j & j <= width (Gauge (C,n)) & (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j))} holds

LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))) meets Lower_Arc C

proof end;

theorem :: JORDAN19:14

for n being Nat

for C being Simple_closed_curve

for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & n > 0 & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Lower_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Upper_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,j))} holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Upper_Arc C

for C being Simple_closed_curve

for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & n > 0 & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Lower_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Upper_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,j))} holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Upper_Arc C

proof end;

theorem :: JORDAN19:15

for n being Nat

for C being Simple_closed_curve

for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & n > 0 & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Lower_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Upper_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,j))} holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C

for C being Simple_closed_curve

for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & n > 0 & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Lower_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Upper_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,j))} holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C

proof end;

theorem Th16: :: JORDAN19:16

for n being Nat

for C being Simple_closed_curve

for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Lower_Seq (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Upper_Arc C

for C being Simple_closed_curve

for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Lower_Seq (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Upper_Arc C

proof end;

theorem Th17: :: JORDAN19:17

for n being Nat

for C being Simple_closed_curve

for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Lower_Seq (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C

for C being Simple_closed_curve

for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Lower_Seq (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C

proof end;

theorem Th18: :: JORDAN19:18

for n being Nat

for C being Simple_closed_curve

for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & n > 0 & (Gauge (C,n)) * (i,k) in Lower_Arc (L~ (Cage (C,n))) & (Gauge (C,n)) * (i,j) in Upper_Arc (L~ (Cage (C,n))) holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Upper_Arc C

for C being Simple_closed_curve

for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & n > 0 & (Gauge (C,n)) * (i,k) in Lower_Arc (L~ (Cage (C,n))) & (Gauge (C,n)) * (i,j) in Upper_Arc (L~ (Cage (C,n))) holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Upper_Arc C

proof end;

theorem Th19: :: JORDAN19:19

for n being Nat

for C being Simple_closed_curve

for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & n > 0 & (Gauge (C,n)) * (i,k) in Lower_Arc (L~ (Cage (C,n))) & (Gauge (C,n)) * (i,j) in Upper_Arc (L~ (Cage (C,n))) holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C

for C being Simple_closed_curve

for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & n > 0 & (Gauge (C,n)) * (i,k) in Lower_Arc (L~ (Cage (C,n))) & (Gauge (C,n)) * (i,j) in Upper_Arc (L~ (Cage (C,n))) holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C

proof end;

theorem Th20: :: JORDAN19:20

for n being Nat

for C being Simple_closed_curve

for i1, i2, j, k being Nat st 1 < i1 & i1 <= i2 & i2 < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} holds

(LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) meets Upper_Arc C

for C being Simple_closed_curve

for i1, i2, j, k being Nat st 1 < i1 & i1 <= i2 & i2 < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} holds

(LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) meets Upper_Arc C

proof end;

theorem Th21: :: JORDAN19:21

for n being Nat

for C being Simple_closed_curve

for i1, i2, j, k being Nat st 1 < i1 & i1 <= i2 & i2 < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} holds

(LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) meets Lower_Arc C

for C being Simple_closed_curve

for i1, i2, j, k being Nat st 1 < i1 & i1 <= i2 & i2 < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} holds

(LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) meets Lower_Arc C

proof end;

theorem Th22: :: JORDAN19:22

for n being Nat

for C being Simple_closed_curve

for i1, i2, j, k being Nat st 1 < i2 & i2 <= i1 & i1 < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} holds

(LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) meets Upper_Arc C

for C being Simple_closed_curve

for i1, i2, j, k being Nat st 1 < i2 & i2 <= i1 & i1 < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} holds

(LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) meets Upper_Arc C

proof end;

theorem Th23: :: JORDAN19:23

for n being Nat

for C being Simple_closed_curve

for i1, i2, j, k being Nat st 1 < i2 & i2 <= i1 & i1 < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} holds

(LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) meets Lower_Arc C

for C being Simple_closed_curve

for i1, i2, j, k being Nat st 1 < i2 & i2 <= i1 & i1 < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} holds

(LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) meets Lower_Arc C

proof end;

theorem Th24: :: JORDAN19:24

for n being Nat

for C being Simple_closed_curve

for i1, i2, j, k being Nat st 1 < i1 & i1 < len (Gauge (C,(n + 1))) & 1 < i2 & i2 < len (Gauge (C,(n + 1))) & 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (i1,k) in Lower_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (i2,j) in Upper_Arc (L~ (Cage (C,(n + 1)))) holds

(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Lower_Arc C

for C being Simple_closed_curve

for i1, i2, j, k being Nat st 1 < i1 & i1 < len (Gauge (C,(n + 1))) & 1 < i2 & i2 < len (Gauge (C,(n + 1))) & 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (i1,k) in Lower_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (i2,j) in Upper_Arc (L~ (Cage (C,(n + 1)))) holds

(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Lower_Arc C

proof end;

theorem Th25: :: JORDAN19:25

for n being Nat

for C being Simple_closed_curve

for i1, i2, j, k being Nat st 1 < i1 & i1 < len (Gauge (C,(n + 1))) & 1 < i2 & i2 < len (Gauge (C,(n + 1))) & 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (i1,k) in Lower_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (i2,j) in Upper_Arc (L~ (Cage (C,(n + 1)))) holds

(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C

for C being Simple_closed_curve

for i1, i2, j, k being Nat st 1 < i1 & i1 < len (Gauge (C,(n + 1))) & 1 < i2 & i2 < len (Gauge (C,(n + 1))) & 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (i1,k) in Lower_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (i2,j) in Upper_Arc (L~ (Cage (C,(n + 1)))) holds

(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C

proof end;

theorem Th26: :: JORDAN19:26

for C being Simple_closed_curve

for p being Point of (TOP-REAL 2) st W-bound C < p `1 & p `1 < E-bound C & p in North_Arc C holds

not p in South_Arc C

for p being Point of (TOP-REAL 2) st W-bound C < p `1 & p `1 < E-bound C & p in North_Arc C holds

not p in South_Arc C

proof end;

theorem :: JORDAN19:27

for C being Simple_closed_curve

for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & p in North_Arc C holds

not p in South_Arc C

for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & p in North_Arc C holds

not p in South_Arc C

proof end;