:: by Robert Milewski

::

:: Received April 5, 2002

:: Copyright (c) 2002-2016 Association of Mizar Users

theorem Th1: :: JORDAN1J:1

for G being Go-board

for i1, i2, j1, j2 being Nat st 1 <= j1 & j1 <= width G & 1 <= j2 & j2 <= width G & 1 <= i1 & i1 < i2 & i2 <= len G holds

(G * (i1,j1)) `1 < (G * (i2,j2)) `1

for i1, i2, j1, j2 being Nat st 1 <= j1 & j1 <= width G & 1 <= j2 & j2 <= width G & 1 <= i1 & i1 < i2 & i2 <= len G holds

(G * (i1,j1)) `1 < (G * (i2,j2)) `1

proof end;

theorem Th2: :: JORDAN1J:2

for G being Go-board

for i1, i2, j1, j2 being Nat st 1 <= i1 & i1 <= len G & 1 <= i2 & i2 <= len G & 1 <= j1 & j1 < j2 & j2 <= width G holds

(G * (i1,j1)) `2 < (G * (i2,j2)) `2

for i1, i2, j1, j2 being Nat st 1 <= i1 & i1 <= len G & 1 <= i2 & i2 <= len G & 1 <= j1 & j1 < j2 & j2 <= width G holds

(G * (i1,j1)) `2 < (G * (i2,j2)) `2

proof end;

registration
end;

theorem Th3: :: JORDAN1J:3

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for n being Nat holds (L~ ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) = {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}

for n being Nat holds (L~ ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) = {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}

proof end;

theorem Th4: :: JORDAN1J:4

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) :- (W-min (L~ (Cage (C,n))))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) :- (W-min (L~ (Cage (C,n))))

proof end;

theorem :: JORDAN1J:5

for n being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( W-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & W-min (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( W-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & W-min (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )

proof end;

theorem :: JORDAN1J:6

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( W-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & W-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( W-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & W-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )

proof end;

theorem Th7: :: JORDAN1J:7

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( N-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & N-min (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( N-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & N-min (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )

proof end;

theorem :: JORDAN1J:8

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( N-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & N-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( N-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & N-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )

proof end;

theorem :: JORDAN1J:9

for n being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( E-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & E-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( E-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & E-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )

proof end;

theorem :: JORDAN1J:10

for n being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( E-max (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & E-max (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( E-max (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & E-max (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )

proof end;

theorem :: JORDAN1J:11

for n being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( E-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & E-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( E-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & E-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )

proof end;

theorem Th12: :: JORDAN1J:12

for n being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( S-max (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & S-max (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( S-max (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & S-max (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )

proof end;

theorem :: JORDAN1J:13

for n being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( S-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & S-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( S-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & S-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )

proof end;

theorem :: JORDAN1J:14

for n being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( W-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & W-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( W-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & W-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )

proof end;

theorem Th15: :: JORDAN1J:15

for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & N-min Y in X holds

N-min X = N-min Y

N-min X = N-min Y

proof end;

theorem Th16: :: JORDAN1J:16

for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & N-max Y in X holds

N-max X = N-max Y

N-max X = N-max Y

proof end;

theorem Th17: :: JORDAN1J:17

for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & E-min Y in X holds

E-min X = E-min Y

E-min X = E-min Y

proof end;

theorem Th18: :: JORDAN1J:18

for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & E-max Y in X holds

E-max X = E-max Y

E-max X = E-max Y

proof end;

theorem Th19: :: JORDAN1J:19

for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & S-min Y in X holds

S-min X = S-min Y

S-min X = S-min Y

proof end;

theorem Th20: :: JORDAN1J:20

for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & S-max Y in X holds

S-max X = S-max Y

S-max X = S-max Y

proof end;

theorem Th21: :: JORDAN1J:21

for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & W-min Y in X holds

W-min X = W-min Y

W-min X = W-min Y

proof end;

theorem Th22: :: JORDAN1J:22

for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & W-max Y in X holds

W-max X = W-max Y

W-max X = W-max Y

proof end;

theorem Th23: :: JORDAN1J:23

for X, Y being non empty compact Subset of (TOP-REAL 2) st N-bound X <= N-bound Y holds

N-bound (X \/ Y) = N-bound Y

N-bound (X \/ Y) = N-bound Y

proof end;

theorem Th24: :: JORDAN1J:24

for X, Y being non empty compact Subset of (TOP-REAL 2) st E-bound X <= E-bound Y holds

E-bound (X \/ Y) = E-bound Y

E-bound (X \/ Y) = E-bound Y

proof end;

theorem Th25: :: JORDAN1J:25

for X, Y being non empty compact Subset of (TOP-REAL 2) st S-bound X <= S-bound Y holds

S-bound (X \/ Y) = S-bound X

S-bound (X \/ Y) = S-bound X

proof end;

theorem Th26: :: JORDAN1J:26

for X, Y being non empty compact Subset of (TOP-REAL 2) st W-bound X <= W-bound Y holds

W-bound (X \/ Y) = W-bound X

W-bound (X \/ Y) = W-bound X

proof end;

theorem :: JORDAN1J:27

for X, Y being non empty compact Subset of (TOP-REAL 2) st N-bound X < N-bound Y holds

N-min (X \/ Y) = N-min Y

N-min (X \/ Y) = N-min Y

proof end;

theorem :: JORDAN1J:28

for X, Y being non empty compact Subset of (TOP-REAL 2) st N-bound X < N-bound Y holds

N-max (X \/ Y) = N-max Y

N-max (X \/ Y) = N-max Y

proof end;

theorem :: JORDAN1J:29

for X, Y being non empty compact Subset of (TOP-REAL 2) st E-bound X < E-bound Y holds

E-min (X \/ Y) = E-min Y

E-min (X \/ Y) = E-min Y

proof end;

theorem :: JORDAN1J:30

for X, Y being non empty compact Subset of (TOP-REAL 2) st E-bound X < E-bound Y holds

E-max (X \/ Y) = E-max Y

E-max (X \/ Y) = E-max Y

proof end;

theorem :: JORDAN1J:31

for X, Y being non empty compact Subset of (TOP-REAL 2) st S-bound X < S-bound Y holds

S-min (X \/ Y) = S-min X

S-min (X \/ Y) = S-min X

proof end;

theorem :: JORDAN1J:32

for X, Y being non empty compact Subset of (TOP-REAL 2) st S-bound X < S-bound Y holds

S-max (X \/ Y) = S-max X

S-max (X \/ Y) = S-max X

proof end;

theorem Th33: :: JORDAN1J:33

for X, Y being non empty compact Subset of (TOP-REAL 2) st W-bound X < W-bound Y holds

W-min (X \/ Y) = W-min X

W-min (X \/ Y) = W-min X

proof end;

theorem :: JORDAN1J:34

for X, Y being non empty compact Subset of (TOP-REAL 2) st W-bound X < W-bound Y holds

W-max (X \/ Y) = W-max X

W-max (X \/ Y) = W-max X

proof end;

theorem Th35: :: JORDAN1J:35

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f holds

(L_Cut (f,p)) /. (len (L_Cut (f,p))) = f /. (len f)

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f holds

(L_Cut (f,p)) /. (len (L_Cut (f,p))) = f /. (len f)

proof end;

theorem Th36: :: JORDAN1J:36

for f being non constant standard special_circular_sequence

for p, q being Point of (TOP-REAL 2)

for g being connected Subset of (TOP-REAL 2) st p in RightComp f & q in LeftComp f & p in g & q in g holds

g meets L~ f

for p, q being Point of (TOP-REAL 2)

for g being connected Subset of (TOP-REAL 2) st p in RightComp f & q in LeftComp f & p in g & q in g holds

g meets L~ f

proof end;

registration

ex b_{1} being being_S-Seq FinSequence of (TOP-REAL 2) st

( not b_{1} is constant & b_{1} is standard & b_{1} is s.c.c. )
end;

cluster V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) non empty non trivial V16() Function-like one-to-one non constant V28() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq s.c.c. standard for FinSequence of the U1 of (TOP-REAL 2);

existence ex b

( not b

proof end;

theorem Th37: :: JORDAN1J:37

for f being S-Sequence_in_R2

for p being Point of (TOP-REAL 2) st p in rng f holds

L_Cut (f,p) = mid (f,(p .. f),(len f))

for p being Point of (TOP-REAL 2) st p in rng f holds

L_Cut (f,p) = mid (f,(p .. f),(len f))

proof end;

theorem Th38: :: JORDAN1J:38

for M being Go-board

for f being S-Sequence_in_R2 st f is_sequence_on M holds

for p being Point of (TOP-REAL 2) st p in rng f holds

R_Cut (f,p) is_sequence_on M

for f being S-Sequence_in_R2 st f is_sequence_on M holds

for p being Point of (TOP-REAL 2) st p in rng f holds

R_Cut (f,p) is_sequence_on M

proof end;

theorem Th39: :: JORDAN1J:39

for M being Go-board

for f being S-Sequence_in_R2 st f is_sequence_on M holds

for p being Point of (TOP-REAL 2) st p in rng f holds

L_Cut (f,p) is_sequence_on M

for f being S-Sequence_in_R2 st f is_sequence_on M holds

for p being Point of (TOP-REAL 2) st p in rng f holds

L_Cut (f,p) is_sequence_on M

proof end;

theorem Th40: :: JORDAN1J:40

for G being Go-board

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds

for i, j being Nat st 1 <= i & i <= len G & 1 <= j & j <= width G & G * (i,j) in L~ f holds

G * (i,j) in rng f

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds

for i, j being Nat st 1 <= i & i <= len G & 1 <= j & j <= width G & G * (i,j) in L~ f holds

G * (i,j) in rng f

proof end;

theorem :: JORDAN1J:41

for f being S-Sequence_in_R2

for g being FinSequence of (TOP-REAL 2) st g is unfolded & g is s.n.c. & g is one-to-one & (L~ f) /\ (L~ g) = {(f /. 1)} & f /. 1 = g /. (len g) & ( for i being Nat st 1 <= i & i + 2 <= len f holds

(LSeg (f,i)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {} ) & ( for i being Nat st 2 <= i & i + 1 <= len g holds

(LSeg (g,i)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {} ) holds

f ^ g is s.c.c.

for g being FinSequence of (TOP-REAL 2) st g is unfolded & g is s.n.c. & g is one-to-one & (L~ f) /\ (L~ g) = {(f /. 1)} & f /. 1 = g /. (len g) & ( for i being Nat st 1 <= i & i + 2 <= len f holds

(LSeg (f,i)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {} ) & ( for i being Nat st 2 <= i & i + 1 <= len g holds

(LSeg (g,i)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {} ) holds

f ^ g is s.c.c.

proof end;

theorem :: JORDAN1J:42

for n being Nat

for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st

( 1 <= i & i + 1 <= len (Gauge (C,n)) & W-min C in cell ((Gauge (C,n)),1,i) & W-min C <> (Gauge (C,n)) * (2,i) )

for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st

( 1 <= i & i + 1 <= len (Gauge (C,n)) & W-min C in cell ((Gauge (C,n)),1,i) & W-min C <> (Gauge (C,n)) * (2,i) )

proof end;

theorem Th43: :: JORDAN1J:43

for f being S-Sequence_in_R2

for p being Point of (TOP-REAL 2) st p in L~ f & f . (len f) in L~ (R_Cut (f,p)) holds

f . (len f) = p

for p being Point of (TOP-REAL 2) st p in L~ f & f . (len f) in L~ (R_Cut (f,p)) holds

f . (len f) = p

proof end;

theorem Th45: :: JORDAN1J:45

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ f holds

(R_Cut (f,p)) /. (len (R_Cut (f,p))) = p

for p being Point of (TOP-REAL 2) st p in L~ f holds

(R_Cut (f,p)) /. (len (R_Cut (f,p))) = p

proof end;

theorem Th46: :: JORDAN1J:46

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ (Upper_Seq (C,n)) & p `1 = E-bound (L~ (Cage (C,n))) holds

p = E-max (L~ (Cage (C,n)))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ (Upper_Seq (C,n)) & p `1 = E-bound (L~ (Cage (C,n))) holds

p = E-max (L~ (Cage (C,n)))

proof end;

theorem :: JORDAN1J:47

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ (Lower_Seq (C,n)) & p `1 = W-bound (L~ (Cage (C,n))) holds

p = W-min (L~ (Cage (C,n)))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ (Lower_Seq (C,n)) & p `1 = W-bound (L~ (Cage (C,n))) holds

p = W-min (L~ (Cage (C,n)))

proof end;

theorem :: JORDAN1J:48

for G being Go-board

for f, g being FinSequence of (TOP-REAL 2)

for k being Nat st 1 <= k & k < len f & f ^ g is_sequence_on G holds

( left_cell ((f ^ g),k,G) = left_cell (f,k,G) & right_cell ((f ^ g),k,G) = right_cell (f,k,G) )

for f, g being FinSequence of (TOP-REAL 2)

for k being Nat st 1 <= k & k < len f & f ^ g is_sequence_on G holds

( left_cell ((f ^ g),k,G) = left_cell (f,k,G) & right_cell ((f ^ g),k,G) = right_cell (f,k,G) )

proof end;

theorem Th49: :: JORDAN1J:49

for D being set

for f, g being FinSequence of D

for i being Nat st i <= len f holds

(f ^' g) | i = f | i

for f, g being FinSequence of D

for i being Nat st i <= len f holds

(f ^' g) | i = f | i

proof end;

theorem Th51: :: JORDAN1J:51

for G being Go-board

for f, g being FinSequence of (TOP-REAL 2)

for k being Nat st 1 <= k & k < len f & f ^' g is_sequence_on G holds

( left_cell ((f ^' g),k,G) = left_cell (f,k,G) & right_cell ((f ^' g),k,G) = right_cell (f,k,G) )

for f, g being FinSequence of (TOP-REAL 2)

for k being Nat st 1 <= k & k < len f & f ^' g is_sequence_on G holds

( left_cell ((f ^' g),k,G) = left_cell (f,k,G) & right_cell ((f ^' g),k,G) = right_cell (f,k,G) )

proof end;

theorem Th52: :: JORDAN1J:52

for G being Go-board

for f being S-Sequence_in_R2

for p being Point of (TOP-REAL 2)

for k being Nat st 1 <= k & k < p .. f & f is_sequence_on G & p in rng f holds

( left_cell ((R_Cut (f,p)),k,G) = left_cell (f,k,G) & right_cell ((R_Cut (f,p)),k,G) = right_cell (f,k,G) )

for f being S-Sequence_in_R2

for p being Point of (TOP-REAL 2)

for k being Nat st 1 <= k & k < p .. f & f is_sequence_on G & p in rng f holds

( left_cell ((R_Cut (f,p)),k,G) = left_cell (f,k,G) & right_cell ((R_Cut (f,p)),k,G) = right_cell (f,k,G) )

proof end;

theorem Th53: :: JORDAN1J:53

for G being Go-board

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2)

for k being Nat st 1 <= k & k < p .. f & f is_sequence_on G holds

( left_cell ((f -: p),k,G) = left_cell (f,k,G) & right_cell ((f -: p),k,G) = right_cell (f,k,G) )

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2)

for k being Nat st 1 <= k & k < p .. f & f is_sequence_on G holds

( left_cell ((f -: p),k,G) = left_cell (f,k,G) & right_cell ((f -: p),k,G) = right_cell (f,k,G) )

proof end;

theorem Th54: :: JORDAN1J:54

for f, g being FinSequence of (TOP-REAL 2) st f is unfolded & f is s.n.c. & f is one-to-one & g is unfolded & g is s.n.c. & g is one-to-one & f /. (len f) = g /. 1 & (L~ f) /\ (L~ g) = {(g /. 1)} holds

f ^' g is s.n.c.

f ^' g is s.n.c.

proof end;

theorem Th55: :: JORDAN1J:55

for f, g being FinSequence of (TOP-REAL 2) st f is one-to-one & g is one-to-one & (rng f) /\ (rng g) c= {(g /. 1)} holds

f ^' g is one-to-one

f ^' g is one-to-one

proof end;

theorem Th56: :: JORDAN1J:56

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in rng f & p <> f . 1 holds

(Index (p,f)) + 1 = p .. f

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in rng f & p <> f . 1 holds

(Index (p,f)) + 1 = p .. f

proof end;

theorem Th57: :: JORDAN1J:57

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

j <> k

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

j <> k

proof end;

theorem Th58: :: JORDAN1J:58

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)) & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j))} holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C

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)) & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j))} holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C

proof end;

theorem Th59: :: JORDAN1J:59

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)) & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j))} holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Upper_Arc C

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)) & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j))} holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Upper_Arc C

proof end;

theorem Th60: :: JORDAN1J:60

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 & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Upper_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Lower_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,j))} holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C

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 & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Upper_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Lower_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,j))} holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C

proof end;

theorem Th61: :: JORDAN1J:61

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 & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Upper_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Lower_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,j))} holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Upper_Arc C

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 & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Upper_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Lower_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,j))} holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Upper_Arc C

proof end;

theorem :: JORDAN1J:62

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for j being Nat st (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Upper_Arc (L~ (Cage (C,(n + 1)))) & 1 <= j & j <= width (Gauge (C,(n + 1))) holds

LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))) meets Lower_Arc (L~ (Cage (C,(n + 1))))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for j being Nat st (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Upper_Arc (L~ (Cage (C,(n + 1)))) & 1 <= j & j <= width (Gauge (C,(n + 1))) holds

LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))) meets Lower_Arc (L~ (Cage (C,(n + 1))))

proof end;

theorem :: JORDAN1J:63

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))) & (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Upper_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k))} & (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Lower_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))} 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

for C being Simple_closed_curve

for j, k being Nat st 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Upper_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k))} & (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Lower_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))} 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 :: JORDAN1J:64

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))) & (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Upper_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k))} & (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Lower_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))} 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

for C being Simple_closed_curve

for j, k being Nat st 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Upper_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k))} & (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Lower_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))} 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;

:: Moved from JORDAN, AG 20.01.2006

theorem :: JORDAN1J:65

for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & ( W-min Y in X or W-max Y in X ) holds

W-bound X = W-bound Y

W-bound X = W-bound Y

proof end;

theorem :: JORDAN1J:66

for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & ( E-min Y in X or E-max Y in X ) holds

E-bound X = E-bound Y

E-bound X = E-bound Y

proof end;

theorem :: JORDAN1J:67

for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & ( N-min Y in X or N-max Y in X ) holds

N-bound X = N-bound Y

N-bound X = N-bound Y

proof end;

theorem :: JORDAN1J:68

for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & ( S-min Y in X or S-max Y in X ) holds

S-bound X = S-bound Y

S-bound X = S-bound Y

proof end;