:: Properties of the Upper and Lower Sequence on the Cage :: by Robert Milewski :: :: Received August 1, 2002 :: Copyright (c) 2002-2012 Association of Mizar Users begin theorem :: JORDAN15:1 for A, B being Subset of (TOP-REAL 2) st A meets B holds proj1 .: A meets proj1 .: B proofend; theorem :: JORDAN15:2 for A, B being Subset of (TOP-REAL 2) for s being real number st A misses B & A c= Horizontal_Line s & B c= Horizontal_Line s holds proj1 .: A misses proj1 .: B proofend; theorem Th3: :: JORDAN15:3 for S being closed Subset of (TOP-REAL 2) st S is bounded holds proj1 .: S is closed proofend; theorem Th4: :: JORDAN15:4 for S being compact Subset of (TOP-REAL 2) holds proj1 .: S is compact proofend; theorem Th5: :: JORDAN15:5 for G being Go-board for i, j, k, j1, k1 being Element of 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))) proofend; theorem Th6: :: JORDAN15:6 for G being Go-board for i, j, k, j1, k1 being Element of 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))) proofend; theorem :: JORDAN15:7 for G being Go-board for j, k, j1, k1 being Element of 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))) proofend; theorem :: JORDAN15:8 for G being Go-board st len G = width G holds for j, k, j1, k1 being Element of 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)))) proofend; theorem Th9: :: JORDAN15:9 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for i, j, k being Element of 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 Element of 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))} ) proofend; theorem :: JORDAN15:10 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for i, j, k being Element of 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 Element of 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))} ) proofend; theorem Th11: :: JORDAN15:11 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for i, j, k being Element of 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 Element of 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))} ) proofend; theorem :: JORDAN15:12 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for i, j, k being Element of 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 Element of 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))} ) proofend; theorem Th13: :: JORDAN15:13 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for i, j, k being Element of 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 Element of 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))} ) proofend; theorem Th14: :: JORDAN15:14 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for i, j, k being Element of 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 Element of 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))} ) proofend; theorem :: JORDAN15:15 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for i, j, k being Element of 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 Element of 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))} ) proofend; theorem :: JORDAN15:16 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for i, j, k being Element of 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 Element of 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))} ) proofend; theorem :: JORDAN15:17 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for i, j, k being Element of 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 Element of 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))} ) proofend; theorem Th18: :: JORDAN15:18 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for i, j, k being Element of 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 Element of 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))} ) proofend; theorem :: JORDAN15:19 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for i, j, k being Element of 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 Element of 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))} ) proofend; theorem Th20: :: JORDAN15:20 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for i, j, k being Element of 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 Element of 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))} ) proofend; theorem Th21: :: JORDAN15:21 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of 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 proofend; theorem Th22: :: JORDAN15:22 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of 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 proofend; theorem Th23: :: JORDAN15:23 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of 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 proofend; theorem Th24: :: JORDAN15:24 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of 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 proofend; theorem :: JORDAN15:25 for n being Element of NAT for C being Simple_closed_curve for j, k being Element of 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 proofend; theorem :: JORDAN15:26 for n being Element of NAT for C being Simple_closed_curve for j, k being Element of 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 proofend; theorem Th27: :: JORDAN15:27 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for i, j, k being Element of 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 proofend; theorem Th28: :: JORDAN15:28 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of 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 proofend; theorem Th29: :: JORDAN15:29 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of 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 proofend; theorem Th30: :: JORDAN15:30 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of 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 proofend; theorem Th31: :: JORDAN15:31 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of 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 proofend; theorem Th32: :: JORDAN15:32 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of 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 proofend; theorem Th33: :: JORDAN15:33 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of 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 proofend; theorem :: JORDAN15:34 for n being Element of NAT for C being Simple_closed_curve for j, k being Element of 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 proofend; theorem :: JORDAN15:35 for n being Element of NAT for C being Simple_closed_curve for j, k being Element of 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 proofend; theorem Th36: :: JORDAN15:36 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of 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 proofend; theorem Th37: :: JORDAN15:37 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of 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 proofend; theorem Th38: :: JORDAN15:38 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of 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 proofend; theorem Th39: :: JORDAN15:39 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of 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 proofend; theorem Th40: :: JORDAN15:40 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of 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 proofend; theorem Th41: :: JORDAN15:41 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of 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 proofend; theorem :: JORDAN15:42 for n being Element of NAT for C being Simple_closed_curve for j, k being Element of 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 proofend; theorem :: JORDAN15:43 for n being Element of NAT for C being Simple_closed_curve for j, k being Element of 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 proofend; theorem Th44: :: JORDAN15:44 for n being Element of NAT for C being Simple_closed_curve for i1, i2, j, k being Element of 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 proofend; theorem Th45: :: JORDAN15:45 for n being Element of NAT for C being Simple_closed_curve for i1, i2, j, k being Element of 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 proofend; theorem Th46: :: JORDAN15:46 for n being Element of NAT for C being Simple_closed_curve for i1, i2, j, k being Element of 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 proofend; theorem Th47: :: JORDAN15:47 for n being Element of NAT for C being Simple_closed_curve for i1, i2, j, k being Element of 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 proofend; theorem Th48: :: JORDAN15:48 for n being Element of NAT for C being Simple_closed_curve for i1, i2, j, k being Element of 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 proofend; theorem Th49: :: JORDAN15:49 for n being Element of NAT for C being Simple_closed_curve for i1, i2, j, k being Element of 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 proofend; theorem :: JORDAN15:50 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of 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 proofend; theorem :: JORDAN15:51 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of 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 proofend;