:: Bounding Boxes for Special Sequences in ${\calE}^2$
:: by Yatsuka Nakamura and Adam Grabowski
::
:: Received June 8, 1998
:: Copyright (c) 1998-2011 Association of Mizar Users

begin

theorem :: JORDAN5D:1

canceled;

theorem :: JORDAN5D:2

canceled;

theorem Th3: :: JORDAN5D:3

for n being Element of NAT
for h being FinSequence of (TOP-REAL n) st len h >= 2 holds
h /. (len h) in LSeg (h,((len h) -' 1))

proof end;

theorem Th4: :: JORDAN5D:4

for i being Element of NAT st 3 <= i holds
i mod (i -' 1) = 1

proof end;

theorem Th5: :: JORDAN5D:5

for p being Point of (TOP-REAL 2)
for h being non constant standard special_circular_sequence st p in rng h holds
ex i being Element of NAT st
( 1 <= i & i + 1 <= len h & h . i = p )

proof end;

theorem Th6: :: JORDAN5D:6

for r being Real
for g being FinSequence of REAL st r in rng g holds
( (Incr g) . 1 <= r & r <= (Incr g) . (len (Incr g)) )

proof end;

theorem Th7: :: JORDAN5D:7

for h being non constant standard special_circular_sequence
for i, I being Element of NAT st 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) holds
( ((GoB h) * (1,I)) `1 <= (h /. i) `1 & (h /. i) `1 <= ((GoB h) * ((len (GoB h)),I)) `1 )

proof end;

theorem Th8: :: JORDAN5D:8

for h being non constant standard special_circular_sequence
for i, I being Element of NAT st 1 <= i & i <= len h & 1 <= I & I <= len (GoB h) holds
( ((GoB h) * (I,1)) `2 <= (h /. i) `2 & (h /. i) `2 <= ((GoB h) * (I,(width (GoB h)))) `2 )

proof end;

theorem Th9: :: JORDAN5D:9

for f being non empty FinSequence of (TOP-REAL 2)
for i being Element of NAT st 1 <= i & i <= len (GoB f) holds
ex k, j being Element of NAT st
( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )

proof end;

theorem Th10: :: JORDAN5D:10

for f being non empty FinSequence of (TOP-REAL 2)
for j being Element of NAT st 1 <= j & j <= width (GoB f) holds
ex k, i being Element of NAT st
( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )

proof end;

theorem Th11: :: JORDAN5D:11

for f being non empty FinSequence of (TOP-REAL 2)
for i, j being Element of NAT st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds
ex k being Element of NAT st
( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `1 = ((GoB f) * (i,j)) `1 )

proof end;

theorem Th12: :: JORDAN5D:12

for f being non empty FinSequence of (TOP-REAL 2)
for i, j being Element of NAT st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds
ex k being Element of NAT st
( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `2 = ((GoB f) * (i,j)) `2 )

proof end;

begin

theorem Th13: :: JORDAN5D:13

for h being non constant standard special_circular_sequence
for i being Element of NAT st 1 <= i & i <= len h holds
( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) )

proof end;

theorem Th14: :: JORDAN5D:14

for h being non constant standard special_circular_sequence
for i being Element of NAT st 1 <= i & i <= len h holds
( W-bound (L~ h) <= (h /. i) `1 & (h /. i) `1 <= E-bound (L~ h) )

proof end;

theorem Th15: :: JORDAN5D:15

for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ h) & q in L~ h ) } holds
X = (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h)))

proof end;

theorem Th16: :: JORDAN5D:16

for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ h) & q in L~ h ) } holds
X = (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h)))

proof end;

theorem Th17: :: JORDAN5D:17

for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ h) & q in L~ h ) } holds
X = (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h)))

proof end;

theorem Th18: :: JORDAN5D:18

for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ h) & q in L~ h ) } holds
X = (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h)))

proof end;

theorem Th19: :: JORDAN5D:19

for g being FinSequence of (TOP-REAL 2)
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } holds
X = (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g))

proof end;

theorem Th20: :: JORDAN5D:20

for g being FinSequence of (TOP-REAL 2)
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ g } holds
X = (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g))

proof end;

theorem :: JORDAN5D:21

for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ h) & q in L~ h ) } holds
lower_bound X = lower_bound (proj2 | (W-most (L~ h))) by Th15;

theorem :: JORDAN5D:22

for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ h) & q in L~ h ) } holds
upper_bound X = upper_bound (proj2 | (W-most (L~ h))) by Th15;

theorem :: JORDAN5D:23

for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ h) & q in L~ h ) } holds
lower_bound X = lower_bound (proj2 | (E-most (L~ h))) by Th16;

theorem :: JORDAN5D:24

for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ h) & q in L~ h ) } holds
upper_bound X = upper_bound (proj2 | (E-most (L~ h))) by Th16;

theorem :: JORDAN5D:25

for g being FinSequence of (TOP-REAL 2)
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } holds
lower_bound X = lower_bound (proj1 | (L~ g)) by Th19;

theorem :: JORDAN5D:26

for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ h) & q in L~ h ) } holds
lower_bound X = lower_bound (proj1 | (S-most (L~ h))) by Th18;

theorem :: JORDAN5D:27

for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ h) & q in L~ h ) } holds
upper_bound X = upper_bound (proj1 | (S-most (L~ h))) by Th18;

theorem :: JORDAN5D:28

for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ h) & q in L~ h ) } holds
lower_bound X = lower_bound (proj1 | (N-most (L~ h))) by Th17;

theorem :: JORDAN5D:29

for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ h) & q in L~ h ) } holds
upper_bound X = upper_bound (proj1 | (N-most (L~ h))) by Th17;

theorem :: JORDAN5D:30

for g being FinSequence of (TOP-REAL 2)
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ g } holds
lower_bound X = lower_bound (proj2 | (L~ g)) by Th20;

theorem :: JORDAN5D:31

for g being FinSequence of (TOP-REAL 2)
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } holds
upper_bound X = upper_bound (proj1 | (L~ g)) by Th19;

theorem :: JORDAN5D:32

for g being FinSequence of (TOP-REAL 2)
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ g } holds
upper_bound X = upper_bound (proj2 | (L~ g)) by Th20;

theorem Th33: :: JORDAN5D:33

for p being Point of (TOP-REAL 2)
for h being non constant standard special_circular_sequence
for I being Element of NAT st p in L~ h & 1 <= I & I <= width (GoB h) holds
((GoB h) * (1,I)) `1 <= p `1

proof end;

theorem Th34: :: JORDAN5D:34

for p being Point of (TOP-REAL 2)
for h being non constant standard special_circular_sequence
for I being Element of NAT st p in L~ h & 1 <= I & I <= width (GoB h) holds
p `1 <= ((GoB h) * ((len (GoB h)),I)) `1

proof end;

theorem Th35: :: JORDAN5D:35

for p being Point of (TOP-REAL 2)
for h being non constant standard special_circular_sequence
for I being Element of NAT st p in L~ h & 1 <= I & I <= len (GoB h) holds
((GoB h) * (I,1)) `2 <= p `2

proof end;

theorem Th36: :: JORDAN5D:36

for p being Point of (TOP-REAL 2)
for h being non constant standard special_circular_sequence
for I being Element of NAT st p in L~ h & 1 <= I & I <= len (GoB h) holds
p `2 <= ((GoB h) * (I,(width (GoB h)))) `2

proof end;

theorem Th37: :: JORDAN5D:37

for h being non constant standard special_circular_sequence
for i, j being Element of NAT st 1 <= i & i <= len (GoB h) & 1 <= j & j <= width (GoB h) holds
ex q being Point of (TOP-REAL 2) st
( q `1 = ((GoB h) * (i,j)) `1 & q in L~ h )

proof end;

theorem Th38: :: JORDAN5D:38

for h being non constant standard special_circular_sequence
for i, j being Element of NAT st 1 <= i & i <= len (GoB h) & 1 <= j & j <= width (GoB h) holds
ex q being Point of (TOP-REAL 2) st
( q `2 = ((GoB h) * (i,j)) `2 & q in L~ h )

proof end;

theorem Th39: :: JORDAN5D:39

for h being non constant standard special_circular_sequence holds W-bound (L~ h) = ((GoB h) * (1,1)) `1

proof end;

theorem Th40: :: JORDAN5D:40

for h being non constant standard special_circular_sequence holds S-bound (L~ h) = ((GoB h) * (1,1)) `2

proof end;

theorem Th41: :: JORDAN5D:41

for h being non constant standard special_circular_sequence holds E-bound (L~ h) = ((GoB h) * ((len (GoB h)),1)) `1

proof end;

theorem Th42: :: JORDAN5D:42

for h being non constant standard special_circular_sequence holds N-bound (L~ h) = ((GoB h) * (1,(width (GoB h)))) `2

proof end;

theorem Th43: :: JORDAN5D:43

for f being non empty FinSequence of (TOP-REAL 2)
for i, I, i1 being Element of NAT
for Y being non empty finite Subset of NAT st 1 <= i & i <= len f & 1 <= I & I <= len (GoB f) & Y = { j where j is Element of NAT : ( [I,j] in Indices (GoB f) & ex k being Element of NAT st
( k in dom f & f /. k = (GoB f) * (I,j) ) ) } & (f /. i) `1 = ((GoB f) * (I,1)) `1 & i1 = min Y holds
((GoB f) * (I,i1)) `2 <= (f /. i) `2

proof end;

theorem Th44: :: JORDAN5D:44

for h being non constant standard special_circular_sequence
for i, I, i1 being Element of NAT
for Y being non empty finite Subset of NAT st 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) & Y = { j where j is Element of NAT : ( [j,I] in Indices (GoB h) & ex k being Element of NAT st
( k in dom h & h /. k = (GoB h) * (j,I) ) ) } & (h /. i) `2 = ((GoB h) * (1,I)) `2 & i1 = min Y holds
((GoB h) * (i1,I)) `1 <= (h /. i) `1

proof end;

theorem Th45: :: JORDAN5D:45

for h being non constant standard special_circular_sequence
for i, I, i1 being Element of NAT
for Y being non empty finite Subset of NAT st 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) & Y = { j where j is Element of NAT : ( [j,I] in Indices (GoB h) & ex k being Element of NAT st
( k in dom h & h /. k = (GoB h) * (j,I) ) ) } & (h /. i) `2 = ((GoB h) * (1,I)) `2 & i1 = max Y holds
((GoB h) * (i1,I)) `1 >= (h /. i) `1

proof end;

theorem Th46: :: JORDAN5D:46

for f being non empty FinSequence of (TOP-REAL 2)
for i, I, i1 being Element of NAT
for Y being non empty finite Subset of NAT st 1 <= i & i <= len f & 1 <= I & I <= len (GoB f) & Y = { j where j is Element of NAT : ( [I,j] in Indices (GoB f) & ex k being Element of NAT st
( k in dom f & f /. k = (GoB f) * (I,j) ) ) } & (f /. i) `1 = ((GoB f) * (I,1)) `1 & i1 = max Y holds
((GoB f) * (I,i1)) `2 >= (f /. i) `2

proof end;

Lm1: for i1 being Element of NAT
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `1 = W-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [1,j] in Indices (GoB h) & ex i being Element of NAT st
( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = min Y holds
((GoB h) * (1,i1)) `2 <= p `2

proof end;

Lm2: for i1 being Element of NAT
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `1 = W-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [1,j] in Indices (GoB h) & ex i being Element of NAT st
( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = max Y holds
((GoB h) * (1,i1)) `2 >= p `2

proof end;

Lm3: for i1 being Element of NAT
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `1 = E-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [(len (GoB h)),j] in Indices (GoB h) & ex i being Element of NAT st
( i in dom h & h /. i = (GoB h) * ((len (GoB h)),j) ) ) } & i1 = min Y holds
((GoB h) * ((len (GoB h)),i1)) `2 <= p `2

proof end;

Lm4: for i1 being Element of NAT
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `1 = E-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [(len (GoB h)),j] in Indices (GoB h) & ex i being Element of NAT st
( i in dom h & h /. i = (GoB h) * ((len (GoB h)),j) ) ) } & i1 = max Y holds
((GoB h) * ((len (GoB h)),i1)) `2 >= p `2

proof end;

Lm5: for i1 being Element of NAT
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `2 = S-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,1] in Indices (GoB h) & ex i being Element of NAT st
( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = min Y holds
((GoB h) * (i1,1)) `1 <= p `1

proof end;

Lm6: for i1 being Element of NAT
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `2 = N-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being Element of NAT st
( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = min Y holds
((GoB h) * (i1,(width (GoB h)))) `1 <= p `1

proof end;

Lm7: for h being non constant standard special_circular_sequence
for i1 being Element of NAT
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT st p `2 = S-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,1] in Indices (GoB h) & ex i being Element of NAT st
( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = max Y holds
((GoB h) * (i1,1)) `1 >= p `1

proof end;

Lm8: for h being non constant standard special_circular_sequence
for i1 being Element of NAT
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT st p `2 = N-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being Element of NAT st
( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = max Y holds
((GoB h) * (i1,(width (GoB h)))) `1 >= p `1

proof end;

Lm9: for h being non constant standard special_circular_sequence holds len h >= 2
by GOBOARD7:36, XXREAL_0:2;

begin

definition

let g be non constant standard special_circular_sequence;
func i_s_w g -> Element of NAT means :Def1: :: JORDAN5D:def 1
( [1,it] in Indices (GoB g) & (GoB g) * (1,it) = W-min (L~ g) );
existence
ex b₁ being Element of NAT st
( [1,b₁] in Indices (GoB g) & (GoB g) * (1,b₁) = W-min (L~ g) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st [1,b₁] in Indices (GoB g) & (GoB g) * (1,b₁) = W-min (L~ g) & [1,b₂] in Indices (GoB g) & (GoB g) * (1,b₂) = W-min (L~ g) holds
b₁ = b₂ by GOBOARD1:21;
func i_n_w g -> Element of NAT means :Def2: :: JORDAN5D:def 2
( [1,it] in Indices (GoB g) & (GoB g) * (1,it) = W-max (L~ g) );
existence
ex b₁ being Element of NAT st
( [1,b₁] in Indices (GoB g) & (GoB g) * (1,b₁) = W-max (L~ g) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st [1,b₁] in Indices (GoB g) & (GoB g) * (1,b₁) = W-max (L~ g) & [1,b₂] in Indices (GoB g) & (GoB g) * (1,b₂) = W-max (L~ g) holds
b₁ = b₂ by GOBOARD1:21;
func i_s_e g -> Element of NAT means :Def3: :: JORDAN5D:def 3
( [(len (GoB g)),it] in Indices (GoB g) & (GoB g) * ((len (GoB g)),it) = E-min (L~ g) );
existence
ex b₁ being Element of NAT st
( [(len (GoB g)),b₁] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b₁) = E-min (L~ g) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st [(len (GoB g)),b₁] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b₁) = E-min (L~ g) & [(len (GoB g)),b₂] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b₂) = E-min (L~ g) holds
b₁ = b₂ by GOBOARD1:21;
func i_n_e g -> Element of NAT means :Def4: :: JORDAN5D:def 4
( [(len (GoB g)),it] in Indices (GoB g) & (GoB g) * ((len (GoB g)),it) = E-max (L~ g) );
existence
ex b₁ being Element of NAT st
( [(len (GoB g)),b₁] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b₁) = E-max (L~ g) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st [(len (GoB g)),b₁] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b₁) = E-max (L~ g) & [(len (GoB g)),b₂] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b₂) = E-max (L~ g) holds
b₁ = b₂ by GOBOARD1:21;
func i_w_s g -> Element of NAT means :Def5: :: JORDAN5D:def 5
( [it,1] in Indices (GoB g) & (GoB g) * (it,1) = S-min (L~ g) );
existence
ex b₁ being Element of NAT st
( [b₁,1] in Indices (GoB g) & (GoB g) * (b₁,1) = S-min (L~ g) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st [b₁,1] in Indices (GoB g) & (GoB g) * (b₁,1) = S-min (L~ g) & [b₂,1] in Indices (GoB g) & (GoB g) * (b₂,1) = S-min (L~ g) holds
b₁ = b₂ by GOBOARD1:21;
func i_e_s g -> Element of NAT means :Def6: :: JORDAN5D:def 6
( [it,1] in Indices (GoB g) & (GoB g) * (it,1) = S-max (L~ g) );
existence
ex b₁ being Element of NAT st
( [b₁,1] in Indices (GoB g) & (GoB g) * (b₁,1) = S-max (L~ g) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st [b₁,1] in Indices (GoB g) & (GoB g) * (b₁,1) = S-max (L~ g) & [b₂,1] in Indices (GoB g) & (GoB g) * (b₂,1) = S-max (L~ g) holds
b₁ = b₂ by GOBOARD1:21;
func i_w_n g -> Element of NAT means :Def7: :: JORDAN5D:def 7
( [it,(width (GoB g))] in Indices (GoB g) & (GoB g) * (it,(width (GoB g))) = N-min (L~ g) );
existence
ex b₁ being Element of NAT st
( [b₁,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b₁,(width (GoB g))) = N-min (L~ g) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st [b₁,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b₁,(width (GoB g))) = N-min (L~ g) & [b₂,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b₂,(width (GoB g))) = N-min (L~ g) holds
b₁ = b₂ by GOBOARD1:21;
func i_e_n g -> Element of NAT means :Def8: :: JORDAN5D:def 8
( [it,(width (GoB g))] in Indices (GoB g) & (GoB g) * (it,(width (GoB g))) = N-max (L~ g) );
existence
ex b₁ being Element of NAT st
( [b₁,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b₁,(width (GoB g))) = N-max (L~ g) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st [b₁,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b₁,(width (GoB g))) = N-max (L~ g) & [b₂,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b₂,(width (GoB g))) = N-max (L~ g) holds
b₁ = b₂ by GOBOARD1:21;

end;

:: deftheorem Def1 defines i_s_w JORDAN5D:def 1 :
for g being non constant standard special_circular_sequence
for b₂ being Element of NAT holds
( b₂ = i_s_w g iff ( [1,b₂] in Indices (GoB g) & (GoB g) * (1,b₂) = W-min (L~ g) ) );

:: deftheorem Def2 defines i_n_w JORDAN5D:def 2 :
for g being non constant standard special_circular_sequence
for b₂ being Element of NAT holds
( b₂ = i_n_w g iff ( [1,b₂] in Indices (GoB g) & (GoB g) * (1,b₂) = W-max (L~ g) ) );

:: deftheorem Def3 defines i_s_e JORDAN5D:def 3 :
for g being non constant standard special_circular_sequence
for b₂ being Element of NAT holds
( b₂ = i_s_e g iff ( [(len (GoB g)),b₂] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b₂) = E-min (L~ g) ) );

:: deftheorem Def4 defines i_n_e JORDAN5D:def 4 :
for g being non constant standard special_circular_sequence
for b₂ being Element of NAT holds
( b₂ = i_n_e g iff ( [(len (GoB g)),b₂] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b₂) = E-max (L~ g) ) );

:: deftheorem Def5 defines i_w_s JORDAN5D:def 5 :
for g being non constant standard special_circular_sequence
for b₂ being Element of NAT holds
( b₂ = i_w_s g iff ( [b₂,1] in Indices (GoB g) & (GoB g) * (b₂,1) = S-min (L~ g) ) );

:: deftheorem Def6 defines i_e_s JORDAN5D:def 6 :
for g being non constant standard special_circular_sequence
for b₂ being Element of NAT holds
( b₂ = i_e_s g iff ( [b₂,1] in Indices (GoB g) & (GoB g) * (b₂,1) = S-max (L~ g) ) );

:: deftheorem Def7 defines i_w_n JORDAN5D:def 7 :
for g being non constant standard special_circular_sequence
for b₂ being Element of NAT holds
( b₂ = i_w_n g iff ( [b₂,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b₂,(width (GoB g))) = N-min (L~ g) ) );

:: deftheorem Def8 defines i_e_n JORDAN5D:def 8 :
for g being non constant standard special_circular_sequence
for b₂ being Element of NAT holds
( b₂ = i_e_n g iff ( [b₂,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b₂,(width (GoB g))) = N-max (L~ g) ) );

theorem :: JORDAN5D:47

for h being non constant standard special_circular_sequence holds
( 1 <= i_w_n h & i_w_n h <= len (GoB h) & 1 <= i_e_n h & i_e_n h <= len (GoB h) & 1 <= i_w_s h & i_w_s h <= len (GoB h) & 1 <= i_e_s h & i_e_s h <= len (GoB h) )

proof end;

theorem :: JORDAN5D:48

for h being non constant standard special_circular_sequence holds
( 1 <= i_n_e h & i_n_e h <= width (GoB h) & 1 <= i_s_e h & i_s_e h <= width (GoB h) & 1 <= i_n_w h & i_n_w h <= width (GoB h) & 1 <= i_s_w h & i_s_w h <= width (GoB h) )

proof end;

Lm10: for h being non constant standard special_circular_sequence
for i1, i2 being Element of NAT st 1 <= i1 & i1 + 1 <= len h & 1 <= i2 & i2 + 1 <= len h & h . i1 = h . i2 holds
i1 = i2

proof end;

definition

let g be non constant standard special_circular_sequence;
func n_s_w g -> Element of NAT means :Def9: :: JORDAN5D:def 9
( 1 <= it & it + 1 <= len g & g . it = W-min (L~ g) );
existence
ex b₁ being Element of NAT st
( 1 <= b₁ & b₁ + 1 <= len g & g . b₁ = W-min (L~ g) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st 1 <= b₁ & b₁ + 1 <= len g & g . b₁ = W-min (L~ g) & 1 <= b₂ & b₂ + 1 <= len g & g . b₂ = W-min (L~ g) holds
b₁ = b₂ by Lm10;
func n_n_w g -> Element of NAT means :Def10: :: JORDAN5D:def 10
( 1 <= it & it + 1 <= len g & g . it = W-max (L~ g) );
existence
ex b₁ being Element of NAT st
( 1 <= b₁ & b₁ + 1 <= len g & g . b₁ = W-max (L~ g) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st 1 <= b₁ & b₁ + 1 <= len g & g . b₁ = W-max (L~ g) & 1 <= b₂ & b₂ + 1 <= len g & g . b₂ = W-max (L~ g) holds
b₁ = b₂ by Lm10;
func n_s_e g -> Element of NAT means :Def11: :: JORDAN5D:def 11
( 1 <= it & it + 1 <= len g & g . it = E-min (L~ g) );
existence
ex b₁ being Element of NAT st
( 1 <= b₁ & b₁ + 1 <= len g & g . b₁ = E-min (L~ g) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st 1 <= b₁ & b₁ + 1 <= len g & g . b₁ = E-min (L~ g) & 1 <= b₂ & b₂ + 1 <= len g & g . b₂ = E-min (L~ g) holds
b₁ = b₂ by Lm10;
func n_n_e g -> Element of NAT means :Def12: :: JORDAN5D:def 12
( 1 <= it & it + 1 <= len g & g . it = E-max (L~ g) );
existence
ex b₁ being Element of NAT st
( 1 <= b₁ & b₁ + 1 <= len g & g . b₁ = E-max (L~ g) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st 1 <= b₁ & b₁ + 1 <= len g & g . b₁ = E-max (L~ g) & 1 <= b₂ & b₂ + 1 <= len g & g . b₂ = E-max (L~ g) holds
b₁ = b₂ by Lm10;
func n_w_s g -> Element of NAT means :Def13: :: JORDAN5D:def 13
( 1 <= it & it + 1 <= len g & g . it = S-min (L~ g) );
existence
ex b₁ being Element of NAT st
( 1 <= b₁ & b₁ + 1 <= len g & g . b₁ = S-min (L~ g) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st 1 <= b₁ & b₁ + 1 <= len g & g . b₁ = S-min (L~ g) & 1 <= b₂ & b₂ + 1 <= len g & g . b₂ = S-min (L~ g) holds
b₁ = b₂ by Lm10;
func n_e_s g -> Element of NAT means :Def14: :: JORDAN5D:def 14
( 1 <= it & it + 1 <= len g & g . it = S-max (L~ g) );
existence
ex b₁ being Element of NAT st
( 1 <= b₁ & b₁ + 1 <= len g & g . b₁ = S-max (L~ g) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st 1 <= b₁ & b₁ + 1 <= len g & g . b₁ = S-max (L~ g) & 1 <= b₂ & b₂ + 1 <= len g & g . b₂ = S-max (L~ g) holds
b₁ = b₂ by Lm10;
func n_w_n g -> Element of NAT means :Def15: :: JORDAN5D:def 15
( 1 <= it & it + 1 <= len g & g . it = N-min (L~ g) );
existence
ex b₁ being Element of NAT st
( 1 <= b₁ & b₁ + 1 <= len g & g . b₁ = N-min (L~ g) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st 1 <= b₁ & b₁ + 1 <= len g & g . b₁ = N-min (L~ g) & 1 <= b₂ & b₂ + 1 <= len g & g . b₂ = N-min (L~ g) holds
b₁ = b₂ by Lm10;
func n_e_n g -> Element of NAT means :Def16: :: JORDAN5D:def 16
( 1 <= it & it + 1 <= len g & g . it = N-max (L~ g) );
existence
ex b₁ being Element of NAT st
( 1 <= b₁ & b₁ + 1 <= len g & g . b₁ = N-max (L~ g) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st 1 <= b₁ & b₁ + 1 <= len g & g . b₁ = N-max (L~ g) & 1 <= b₂ & b₂ + 1 <= len g & g . b₂ = N-max (L~ g) holds
b₁ = b₂ by Lm10;

end;

:: deftheorem Def9 defines n_s_w JORDAN5D:def 9 :
for g being non constant standard special_circular_sequence
for b₂ being Element of NAT holds
( b₂ = n_s_w g iff ( 1 <= b₂ & b₂ + 1 <= len g & g . b₂ = W-min (L~ g) ) );

:: deftheorem Def10 defines n_n_w JORDAN5D:def 10 :
for g being non constant standard special_circular_sequence
for b₂ being Element of NAT holds
( b₂ = n_n_w g iff ( 1 <= b₂ & b₂ + 1 <= len g & g . b₂ = W-max (L~ g) ) );

:: deftheorem Def11 defines n_s_e JORDAN5D:def 11 :
for g being non constant standard special_circular_sequence
for b₂ being Element of NAT holds
( b₂ = n_s_e g iff ( 1 <= b₂ & b₂ + 1 <= len g & g . b₂ = E-min (L~ g) ) );

:: deftheorem Def12 defines n_n_e JORDAN5D:def 12 :
for g being non constant standard special_circular_sequence
for b₂ being Element of NAT holds
( b₂ = n_n_e g iff ( 1 <= b₂ & b₂ + 1 <= len g & g . b₂ = E-max (L~ g) ) );

:: deftheorem Def13 defines n_w_s JORDAN5D:def 13 :
for g being non constant standard special_circular_sequence
for b₂ being Element of NAT holds
( b₂ = n_w_s g iff ( 1 <= b₂ & b₂ + 1 <= len g & g . b₂ = S-min (L~ g) ) );

:: deftheorem Def14 defines n_e_s JORDAN5D:def 14 :
for g being non constant standard special_circular_sequence
for b₂ being Element of NAT holds
( b₂ = n_e_s g iff ( 1 <= b₂ & b₂ + 1 <= len g & g . b₂ = S-max (L~ g) ) );

:: deftheorem Def15 defines n_w_n JORDAN5D:def 15 :
for g being non constant standard special_circular_sequence
for b₂ being Element of NAT holds
( b₂ = n_w_n g iff ( 1 <= b₂ & b₂ + 1 <= len g & g . b₂ = N-min (L~ g) ) );

:: deftheorem Def16 defines n_e_n JORDAN5D:def 16 :
for g being non constant standard special_circular_sequence
for b₂ being Element of NAT holds
( b₂ = n_e_n g iff ( 1 <= b₂ & b₂ + 1 <= len g & g . b₂ = N-max (L~ g) ) );

theorem :: JORDAN5D:49

for h being non constant standard special_circular_sequence holds n_w_n h <> n_w_s h

proof end;

theorem :: JORDAN5D:50

for h being non constant standard special_circular_sequence holds n_s_w h <> n_s_e h

proof end;

theorem :: JORDAN5D:51

for h being non constant standard special_circular_sequence holds n_e_n h <> n_e_s h

proof end;

theorem :: JORDAN5D:52

for h being non constant standard special_circular_sequence holds n_n_w h <> n_n_e h

proof end;