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

environ

vocabularies HIDDEN, NUMBERS, SUBSET_1, EUCLID, XBOOLE_0, RELAT_1, PRE_TOPC, MCART_1, FUNCT_1, TARSKI, JORDAN6, REAL_1, RCOMP_1, JORDAN2C, GOBOARD1, XXREAL_0, FINSEQ_1, TREES_1, RLTOPSP1, SPPOL_1, JORDAN1A, RELAT_2, JORDAN8, TOPREAL1, JORDAN1E, MATRIX_1, SEQ_4, PSCOMP_1, XXREAL_2, TOPREAL2, ARYTM_3, CARD_1, JORDAN9, JORDAN3, PARTFUN1, GOBOARD5, ARYTM_1, FINSEQ_4, GRAPH_2, FINSEQ_6, ZFMISC_1, GOBOARD9, GOBOARD2, FINSEQ_5, SPRECT_2, GROUP_2, NAT_1, CONNSP_1;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, NAT_D, FUNCT_1, RELSET_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, XXREAL_2, SEQ_4, MATRIX_0, FINSEQ_6, GRAPH_2, STRUCT_0, PRE_TOPC, RCOMP_1, TOPREAL2, CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID, MEASURE6, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13, SPPOL_1, JORDAN3, JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN1A, JORDAN1E;
definitions TARSKI, XBOOLE_0;
theorems NAT_1, FINSEQ_1, GOBOARD1, FINSEQ_4, EUCLID, FINSEQ_3, SPPOL_2, TARSKI, JORDAN3, PSCOMP_1, FINSEQ_5, FINSEQ_6, GOBOARD7, TOPREAL1, GOBOARD5, SPRECT_2, SPPOL_1, FUNCT_2, GOBOARD9, FINSEQ_2, SUBSET_1, JORDAN4, SPRECT_3, TOPREAL3, JORDAN8, PARTFUN2, SPRECT_1, XBOOLE_0, XBOOLE_1, ZFMISC_1, SEQ_4, GOBRD14, TOPREAL6, JORDAN2C, PRE_TOPC, JORDAN6, JORDAN9, JORDAN1H, JORDAN1A, JORDAN1C, JORDAN1E, JORDAN10, JGRAPH_1, REVROT_1, RCOMP_1, COMPTS_1, ENUMSET1, JORDAN1B, JORDAN1F, JORDAN1G, JORDAN1I, JORDAN1J, GOBOARD3, TOPREAL8, GRAPH_2, SPRECT_5, JORDAN1D, XREAL_1, XXREAL_0, JCT_MISC, PARTFUN1, MATRIX_0, XXREAL_2, NAT_D, XREAL_0, RLTOPSP1;
schemes ;
registrations XBOOLE_0, RELSET_1, NAT_1, MEMBERED, FINSEQ_1, FINSEQ_6, STRUCT_0, COMPTS_1, TOPREAL1, TOPREAL2, GOBOARD2, JORDAN1, SPPOL_2, PSCOMP_1, GOBRD11, TOPREAL5, SPRECT_1, SPRECT_2, REVROT_1, TOPREAL6, JORDAN8, JORDAN1E, JORDAN1J, FUNCT_1, EUCLID, RLTOPSP1, MEASURE6, JORDAN5A, JORDAN2C, XREAL_0, ORDINAL1;
constructors HIDDEN, REAL_1, RCOMP_1, FINSEQ_4, NEWTON, BINARITH, CONNSP_1, REALSET2, GOBOARD2, PSCOMP_1, GRAPH_2, GOBOARD9, JORDAN3, JORDAN5C, JORDAN6, JORDAN2C, JORDAN8, GOBRD13, JORDAN9, JORDAN1A, JORDAN1E, NAT_D, SEQ_4, RELSET_1, CONVEX1, MEASURE6;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities PSCOMP_1;
expansions TARSKI, XBOOLE_0;


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;