:: Properties of the Upper and Lower Sequence on the Cage
:: by Robert Milewski
::
:: Received August 1, 2002
:: Copyright (c) 2002-2021 Association of Mizar Users


theorem :: JORDAN15:1
for A, B being Subset of (TOP-REAL 2) st A meets B holds
proj1 .: A meets proj1 .: B
proof end;

theorem :: JORDAN15:2
for A, B being Subset of (TOP-REAL 2)
for s being Real st A misses B & A c= Horizontal_Line s & B c= Horizontal_Line s holds
proj1 .: A misses proj1 .: B
proof end;

theorem Th3: :: JORDAN15:3
for S being closed Subset of (TOP-REAL 2) st S is bounded holds
proj1 .: S is closed
proof end;

theorem Th4: :: JORDAN15:4
for S being compact Subset of (TOP-REAL 2) holds proj1 .: S is compact
proof end;

theorem Th5: :: JORDAN15:5
for G being Go-board
for i, j, k, j1, k1 being Nat st 1 <= i & i <= len G & 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= width G holds
LSeg ((G * (i,j1)),(G * (i,k1))) c= LSeg ((G * (i,j)),(G * (i,k)))
proof end;

theorem Th6: :: JORDAN15:6
for G being Go-board
for i, j, k, j1, k1 being Nat st 1 <= i & i <= width G & 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= len G holds
LSeg ((G * (j1,i)),(G * (k1,i))) c= LSeg ((G * (j,i)),(G * (k,i)))
proof end;

theorem :: JORDAN15:7
for G being Go-board
for j, k, j1, k1 being Nat st 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= width G holds
LSeg ((G * ((Center G),j1)),(G * ((Center G),k1))) c= LSeg ((G * ((Center G),j)),(G * ((Center G),k)))
proof end;

theorem :: JORDAN15:8
for G being Go-board st len G = width G holds
for j, k, j1, k1 being Nat st 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= len G holds
LSeg ((G * (j1,(Center G))),(G * (k1,(Center G)))) c= LSeg ((G * (j,(Center G))),(G * (k,(Center G))))
proof end;

theorem Th9: :: JORDAN15:9
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
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,j) in L~ (Lower_Seq (C,n)) holds
ex j1 being Nat st
( j <= j1 & j1 <= k & (LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j1))} )
proof end;

theorem :: JORDAN15:10
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
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~ (Upper_Seq (C,n)) holds
ex k1 being Nat st
( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} )
proof end;

theorem Th11: :: JORDAN15:11
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
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,j) in L~ (Lower_Seq (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Upper_Seq (C,n)) holds
ex j1, k1 being Nat st
( j <= j1 & j1 <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j1))} & (LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} )
proof end;

theorem :: JORDAN15:12
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= j & j <= k & k <= len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (j,i) in L~ (Lower_Seq (C,n)) holds
ex j1 being Nat st
( j <= j1 & j1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} )
proof end;

theorem Th13: :: JORDAN15:13
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= j & j <= k & k <= len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) holds
ex k1 being Nat st
( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} )
proof end;

theorem Th14: :: JORDAN15:14
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= j & j <= k & k <= len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (j,i) in L~ (Lower_Seq (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) holds
ex j1, k1 being Nat st
( j <= j1 & j1 <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} )
proof end;

theorem :: JORDAN15:15
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
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,j) in L~ (Upper_Seq (C,n)) holds
ex j1 being Nat st
( j <= j1 & j1 <= k & (LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,j1))} )
proof end;

theorem :: JORDAN15:16
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
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)) holds
ex k1 being Nat st
( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} )
proof end;

theorem :: JORDAN15:17
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
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,j) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Lower_Seq (C,n)) holds
ex j1, k1 being Nat st
( j <= j1 & j1 <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,j1))} & (LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} )
proof end;

theorem Th18: :: JORDAN15:18
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= j & j <= k & k <= len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (j,i) in L~ (Upper_Seq (C,n)) holds
ex j1 being Nat st
( j <= j1 & j1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} )
proof end;

theorem :: JORDAN15:19
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= j & j <= k & k <= len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Lower_Seq (C,n)) holds
ex k1 being Nat st
( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} )
proof end;

theorem Th20: :: JORDAN15:20
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= j & j <= k & k <= len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (j,i) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Lower_Seq (C,n)) holds
ex j1, k1 being Nat st
( j <= j1 & j1 <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} )
proof end;

theorem Th21: :: JORDAN15:21
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~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) holds
LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C
proof end;

theorem Th22: :: JORDAN15:22
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~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) holds
LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Upper_Arc C
proof end;

theorem Th23: :: JORDAN15:23
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 Upper_Arc (L~ (Cage (C,n))) & (Gauge (C,n)) * (i,j) in Lower_Arc (L~ (Cage (C,n))) holds
LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C
proof end;

theorem Th24: :: JORDAN15:24
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 Upper_Arc (L~ (Cage (C,n))) & (Gauge (C,n)) * (i,j) in Lower_Arc (L~ (Cage (C,n))) holds
LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Upper_Arc C
proof end;

theorem :: JORDAN15:25
for n being Nat
for C being Simple_closed_curve
for j, k being Nat st 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k) in Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Lower_Arc (L~ (Cage (C,(n + 1)))) holds
LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k))) meets Lower_Arc C
proof end;

theorem :: JORDAN15:26
for n being Nat
for C being Simple_closed_curve
for j, k being Nat st 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k) in Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Lower_Arc (L~ (Cage (C,(n + 1)))) holds
LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k))) meets Upper_Arc C
proof end;

theorem Th27: :: JORDAN15:27
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 < j & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (j,i) in L~ (Lower_Seq (C,n)) holds
j <> k
proof end;

theorem Th28: :: JORDAN15:28
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (k,i))} & (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (j,i))} holds
LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets Lower_Arc C
proof end;

theorem Th29: :: JORDAN15:29
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (k,i))} & (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (j,i))} holds
LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets Upper_Arc C
proof end;

theorem Th30: :: JORDAN15:30
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (j,i) in L~ (Lower_Seq (C,n)) holds
LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets Lower_Arc C
proof end;

theorem Th31: :: JORDAN15:31
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (j,i) in L~ (Lower_Seq (C,n)) holds
LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets Upper_Arc C
proof end;

theorem Th32: :: JORDAN15:32
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & n > 0 & (Gauge (C,n)) * (k,i) in Upper_Arc (L~ (Cage (C,n))) & (Gauge (C,n)) * (j,i) in Lower_Arc (L~ (Cage (C,n))) holds
LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets Lower_Arc C
proof end;

theorem Th33: :: JORDAN15:33
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & n > 0 & (Gauge (C,n)) * (k,i) in Upper_Arc (L~ (Cage (C,n))) & (Gauge (C,n)) * (j,i) in Lower_Arc (L~ (Cage (C,n))) holds
LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets Upper_Arc C
proof end;

theorem :: JORDAN15:34
for n being Nat
for C being Simple_closed_curve
for j, k being Nat st 1 < j & j <= k & k < len (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (k,(Center (Gauge (C,(n + 1))))) in Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (j,(Center (Gauge (C,(n + 1))))) in Lower_Arc (L~ (Cage (C,(n + 1)))) holds
LSeg (((Gauge (C,(n + 1))) * (j,(Center (Gauge (C,(n + 1)))))),((Gauge (C,(n + 1))) * (k,(Center (Gauge (C,(n + 1))))))) meets Lower_Arc C
proof end;

theorem :: JORDAN15:35
for n being Nat
for C being Simple_closed_curve
for j, k being Nat st 1 < j & j <= k & k < len (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (k,(Center (Gauge (C,(n + 1))))) in Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (j,(Center (Gauge (C,(n + 1))))) in Lower_Arc (L~ (Cage (C,(n + 1)))) holds
LSeg (((Gauge (C,(n + 1))) * (j,(Center (Gauge (C,(n + 1)))))),((Gauge (C,(n + 1))) * (k,(Center (Gauge (C,(n + 1))))))) meets Upper_Arc C
proof end;

theorem Th36: :: JORDAN15:36
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j,i))} & (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (k,i))} holds
LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets Lower_Arc C
proof end;

theorem Th37: :: JORDAN15:37
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j,i))} & (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (k,i))} holds
LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets Upper_Arc C
proof end;

theorem Th38: :: JORDAN15:38
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (j,i) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Lower_Seq (C,n)) holds
LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets Lower_Arc C
proof end;

theorem Th39: :: JORDAN15:39
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (j,i) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Lower_Seq (C,n)) holds
LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets Upper_Arc C
proof end;

theorem Th40: :: JORDAN15:40
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & n > 0 & (Gauge (C,n)) * (j,i) in Upper_Arc (L~ (Cage (C,n))) & (Gauge (C,n)) * (k,i) in Lower_Arc (L~ (Cage (C,n))) holds
LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets Lower_Arc C
proof end;

theorem Th41: :: JORDAN15:41
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & n > 0 & (Gauge (C,n)) * (j,i) in Upper_Arc (L~ (Cage (C,n))) & (Gauge (C,n)) * (k,i) in Lower_Arc (L~ (Cage (C,n))) holds
LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets Upper_Arc C
proof end;

theorem :: JORDAN15:42
for n being Nat
for C being Simple_closed_curve
for j, k being Nat st 1 < j & j <= k & k < len (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (j,(Center (Gauge (C,(n + 1))))) in Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (k,(Center (Gauge (C,(n + 1))))) in Lower_Arc (L~ (Cage (C,(n + 1)))) holds
LSeg (((Gauge (C,(n + 1))) * (j,(Center (Gauge (C,(n + 1)))))),((Gauge (C,(n + 1))) * (k,(Center (Gauge (C,(n + 1))))))) meets Lower_Arc C
proof end;

theorem :: JORDAN15:43
for n being Nat
for C being Simple_closed_curve
for j, k being Nat st 1 < j & j <= k & k < len (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (j,(Center (Gauge (C,(n + 1))))) in Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (k,(Center (Gauge (C,(n + 1))))) in Lower_Arc (L~ (Cage (C,(n + 1)))) holds
LSeg (((Gauge (C,(n + 1))) * (j,(Center (Gauge (C,(n + 1)))))),((Gauge (C,(n + 1))) * (k,(Center (Gauge (C,(n + 1))))))) meets Upper_Arc C
proof end;

theorem Th44: :: JORDAN15:44
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)) * (i2,k))} & ((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)) * (i1,j))} 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 Th45: :: JORDAN15:45
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)) * (i2,k))} & ((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)) * (i1,j))} 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 Th46: :: JORDAN15:46
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)) * (i2,k))} & ((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)) * (i1,j))} 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 Th47: :: JORDAN15:47
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)) * (i2,k))} & ((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)) * (i1,j))} 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 Th48: :: JORDAN15:48
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 Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (i2,j) in Lower_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 Th49: :: JORDAN15:49
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 Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (i2,j) in Lower_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 :: JORDAN15:50
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))) & 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (i,k) in Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Lower_Arc (L~ (Cage (C,(n + 1)))) holds
(LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) \/ (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)),((Gauge (C,(n + 1))) * (i,k)))) meets Upper_Arc C
proof end;

theorem :: JORDAN15:51
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))) & 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (i,k) in Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Lower_Arc (L~ (Cage (C,(n + 1)))) holds
(LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) \/ (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)),((Gauge (C,(n + 1))) * (i,k)))) meets Lower_Arc C
proof end;