:: 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;