:: Properties of the Upper and Lower Sequence on the Cage
:: by Robert Milewski
::
:: Received August 1, 2002
:: Copyright (c) 2002 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 number 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 :: JORDAN15:5

canceled;

theorem :: JORDAN15:6

canceled;

theorem Th7: :: JORDAN15:7

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)

proof end;

theorem Th8: :: JORDAN15:8

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)

proof end;

theorem :: JORDAN15:9

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)

proof end;

theorem :: JORDAN15:10

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))

proof end;

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) 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)} )

proof end;

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 <= 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)} )

proof end;

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 <= 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)} )

proof end;

theorem :: 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) 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)} )

proof end;

theorem Th15: :: 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 <= 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)} )

proof end;

theorem Th16: :: 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 <= 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)} )

proof end;

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) 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)} )

proof end;

theorem :: 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 <= 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)} )

proof end;

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 <= 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)} )

proof end;

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) 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)} )

proof end;

theorem :: JORDAN15:21

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)} )

proof end;

theorem Th22: :: JORDAN15:22

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)} )

proof end;

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) & (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 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) & (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 Th25: :: JORDAN15:25

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

proof end;

theorem Th26: :: JORDAN15:26

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

proof end;

theorem :: JORDAN15:27

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

proof end;

theorem :: JORDAN15:28

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

proof end;

theorem Th29: :: JORDAN15:29

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

proof end;

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) & (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 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) & (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 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) & (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 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) & (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 Th34: :: JORDAN15:34

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

proof end;

theorem Th35: :: JORDAN15:35

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

proof end;

theorem :: JORDAN15:36

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

proof end;

theorem :: JORDAN15:37

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

proof end;

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) & (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 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) & (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 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) & (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 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) & (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 Th42: :: JORDAN15:42

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

proof end;

theorem Th43: :: JORDAN15:43

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

proof end;

theorem :: JORDAN15:44

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

proof end;

theorem :: JORDAN15:45

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

proof end;

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 < 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 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 < 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 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 < 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 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 < 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 Th50: :: JORDAN15:50

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

proof end;

theorem Th51: :: JORDAN15:51

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

proof end;

theorem :: JORDAN15:52

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

proof end;

theorem :: JORDAN15:53

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

proof end;