:: JORDAN5D semantic presentation

theorem Th1: :: JORDAN5D:1
canceled;

theorem Th2: :: JORDAN5D:2
canceled;

theorem Th3: :: JORDAN5D:3
for b1 being Nat
for b2 being FinSequence of (TOP-REAL b1) st len b2 >= 2 holds
b2 /. (len b2) in LSeg b2,((len b2) -' 1)
proof end;

theorem Th4: :: JORDAN5D:4
for b1 being Nat st 3 <= b1 holds
b1 mod (b1 -' 1) = 1
proof end;

theorem Th5: :: JORDAN5D:5
for b1 being Point of (TOP-REAL 2)
for b2 being non constant standard special_circular_sequence st b1 in rng b2 holds
ex b3 being Nat st
( 1 <= b3 & b3 + 1 <= len b2 & b2 . b3 = b1 )
proof end;

theorem Th6: :: JORDAN5D:6
for b1 being Real
for b2 being FinSequence of REAL st b1 in rng b2 holds
( (Incr b2) . 1 <= b1 & b1 <= (Incr b2) . (len (Incr b2)) )
proof end;

theorem Th7: :: JORDAN5D:7
for b1 being non constant standard special_circular_sequence
for b2, b3 being Nat st 1 <= b2 & b2 <= len b1 & 1 <= b3 & b3 <= width (GoB b1) holds
( ((GoB b1) * 1,b3) `1 <= (b1 /. b2) `1 & (b1 /. b2) `1 <= ((GoB b1) * (len (GoB b1)),b3) `1 )
proof end;

theorem Th8: :: JORDAN5D:8
for b1 being non constant standard special_circular_sequence
for b2, b3 being Nat st 1 <= b2 & b2 <= len b1 & 1 <= b3 & b3 <= len (GoB b1) holds
( ((GoB b1) * b3,1) `2 <= (b1 /. b2) `2 & (b1 /. b2) `2 <= ((GoB b1) * b3,(width (GoB b1))) `2 )
proof end;

theorem Th9: :: JORDAN5D:9
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2 being Nat st 1 <= b2 & b2 <= len (GoB b1) holds
ex b3, b4 being Nat st
( b3 in dom b1 & [b2,b4] in Indices (GoB b1) & b1 /. b3 = (GoB b1) * b2,b4 )
proof end;

theorem Th10: :: JORDAN5D:10
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2 being Nat st 1 <= b2 & b2 <= width (GoB b1) holds
ex b3, b4 being Nat st
( b3 in dom b1 & [b4,b2] in Indices (GoB b1) & b1 /. b3 = (GoB b1) * b4,b2 )
proof end;

theorem Th11: :: JORDAN5D:11
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2, b3 being Nat st 1 <= b2 & b2 <= len (GoB b1) & 1 <= b3 & b3 <= width (GoB b1) holds
ex b4 being Nat st
( b4 in dom b1 & [b2,b3] in Indices (GoB b1) & (b1 /. b4) `1 = ((GoB b1) * b2,b3) `1 )
proof end;

theorem Th12: :: JORDAN5D:12
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2, b3 being Nat st 1 <= b2 & b2 <= len (GoB b1) & 1 <= b3 & b3 <= width (GoB b1) holds
ex b4 being Nat st
( b4 in dom b1 & [b2,b3] in Indices (GoB b1) & (b1 /. b4) `2 = ((GoB b1) * b2,b3) `2 )
proof end;

theorem Th13: :: JORDAN5D:13
for b1 being non constant standard special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 <= len b1 holds
( S-bound (L~ b1) <= (b1 /. b2) `2 & (b1 /. b2) `2 <= N-bound (L~ b1) )
proof end;

theorem Th14: :: JORDAN5D:14
for b1 being non constant standard special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 <= len b1 holds
( W-bound (L~ b1) <= (b1 /. b2) `1 & (b1 /. b2) `1 <= E-bound (L~ b1) )
proof end;

theorem Th15: :: JORDAN5D:15
for b1 being non constant standard special_circular_sequence
for b2 being Subset of REAL st b2 = { (b3 `2 ) where B is Point of (TOP-REAL 2) : ( b3 `1 = W-bound (L~ b1) & b3 in L~ b1 ) } holds
b2 = (proj2 || (W-most (L~ b1))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ b1)))
proof end;

theorem Th16: :: JORDAN5D:16
for b1 being non constant standard special_circular_sequence
for b2 being Subset of REAL st b2 = { (b3 `2 ) where B is Point of (TOP-REAL 2) : ( b3 `1 = E-bound (L~ b1) & b3 in L~ b1 ) } holds
b2 = (proj2 || (E-most (L~ b1))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ b1)))
proof end;

theorem Th17: :: JORDAN5D:17
for b1 being non constant standard special_circular_sequence
for b2 being Subset of REAL st b2 = { (b3 `1 ) where B is Point of (TOP-REAL 2) : ( b3 `2 = N-bound (L~ b1) & b3 in L~ b1 ) } holds
b2 = (proj1 || (N-most (L~ b1))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ b1)))
proof end;

theorem Th18: :: JORDAN5D:18
for b1 being non constant standard special_circular_sequence
for b2 being Subset of REAL st b2 = { (b3 `1 ) where B is Point of (TOP-REAL 2) : ( b3 `2 = S-bound (L~ b1) & b3 in L~ b1 ) } holds
b2 = (proj1 || (S-most (L~ b1))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ b1)))
proof end;

theorem Th19: :: JORDAN5D:19
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Subset of REAL st b2 = { (b3 `1 ) where B is Point of (TOP-REAL 2) : b3 in L~ b1 } holds
b2 = (proj1 || (L~ b1)) .: the carrier of ((TOP-REAL 2) | (L~ b1))
proof end;

theorem Th20: :: JORDAN5D:20
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Subset of REAL st b2 = { (b3 `2 ) where B is Point of (TOP-REAL 2) : b3 in L~ b1 } holds
b2 = (proj2 || (L~ b1)) .: the carrier of ((TOP-REAL 2) | (L~ b1))
proof end;

theorem Th21: :: JORDAN5D:21
for b1 being non constant standard special_circular_sequence
for b2 being Subset of REAL st b2 = { (b3 `2 ) where B is Point of (TOP-REAL 2) : ( b3 `1 = W-bound (L~ b1) & b3 in L~ b1 ) } holds
lower_bound b2 = inf (proj2 || (W-most (L~ b1)))
proof end;

theorem Th22: :: JORDAN5D:22
for b1 being non constant standard special_circular_sequence
for b2 being Subset of REAL st b2 = { (b3 `2 ) where B is Point of (TOP-REAL 2) : ( b3 `1 = W-bound (L~ b1) & b3 in L~ b1 ) } holds
upper_bound b2 = sup (proj2 || (W-most (L~ b1)))
proof end;

theorem Th23: :: JORDAN5D:23
for b1 being non constant standard special_circular_sequence
for b2 being Subset of REAL st b2 = { (b3 `2 ) where B is Point of (TOP-REAL 2) : ( b3 `1 = E-bound (L~ b1) & b3 in L~ b1 ) } holds
lower_bound b2 = inf (proj2 || (E-most (L~ b1)))
proof end;

theorem Th24: :: JORDAN5D:24
for b1 being non constant standard special_circular_sequence
for b2 being Subset of REAL st b2 = { (b3 `2 ) where B is Point of (TOP-REAL 2) : ( b3 `1 = E-bound (L~ b1) & b3 in L~ b1 ) } holds
upper_bound b2 = sup (proj2 || (E-most (L~ b1)))
proof end;

theorem Th25: :: JORDAN5D:25
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Subset of REAL st b2 = { (b3 `1 ) where B is Point of (TOP-REAL 2) : b3 in L~ b1 } holds
lower_bound b2 = inf (proj1 || (L~ b1))
proof end;

theorem Th26: :: JORDAN5D:26
for b1 being non constant standard special_circular_sequence
for b2 being Subset of REAL st b2 = { (b3 `1 ) where B is Point of (TOP-REAL 2) : ( b3 `2 = S-bound (L~ b1) & b3 in L~ b1 ) } holds
lower_bound b2 = inf (proj1 || (S-most (L~ b1)))
proof end;

theorem Th27: :: JORDAN5D:27
for b1 being non constant standard special_circular_sequence
for b2 being Subset of REAL st b2 = { (b3 `1 ) where B is Point of (TOP-REAL 2) : ( b3 `2 = S-bound (L~ b1) & b3 in L~ b1 ) } holds
upper_bound b2 = sup (proj1 || (S-most (L~ b1)))
proof end;

theorem Th28: :: JORDAN5D:28
for b1 being non constant standard special_circular_sequence
for b2 being Subset of REAL st b2 = { (b3 `1 ) where B is Point of (TOP-REAL 2) : ( b3 `2 = N-bound (L~ b1) & b3 in L~ b1 ) } holds
lower_bound b2 = inf (proj1 || (N-most (L~ b1)))
proof end;

theorem Th29: :: JORDAN5D:29
for b1 being non constant standard special_circular_sequence
for b2 being Subset of REAL st b2 = { (b3 `1 ) where B is Point of (TOP-REAL 2) : ( b3 `2 = N-bound (L~ b1) & b3 in L~ b1 ) } holds
upper_bound b2 = sup (proj1 || (N-most (L~ b1)))
proof end;

theorem Th30: :: JORDAN5D:30
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Subset of REAL st b2 = { (b3 `2 ) where B is Point of (TOP-REAL 2) : b3 in L~ b1 } holds
lower_bound b2 = inf (proj2 || (L~ b1))
proof end;

theorem Th31: :: JORDAN5D:31
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Subset of REAL st b2 = { (b3 `1 ) where B is Point of (TOP-REAL 2) : b3 in L~ b1 } holds
upper_bound b2 = sup (proj1 || (L~ b1))
proof end;

theorem Th32: :: JORDAN5D:32
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Subset of REAL st b2 = { (b3 `2 ) where B is Point of (TOP-REAL 2) : b3 in L~ b1 } holds
upper_bound b2 = sup (proj2 || (L~ b1))
proof end;

theorem Th33: :: JORDAN5D:33
for b1 being Point of (TOP-REAL 2)
for b2 being non constant standard special_circular_sequence
for b3 being Nat st b1 in L~ b2 & 1 <= b3 & b3 <= width (GoB b2) holds
((GoB b2) * 1,b3) `1 <= b1 `1
proof end;

theorem Th34: :: JORDAN5D:34
for b1 being Point of (TOP-REAL 2)
for b2 being non constant standard special_circular_sequence
for b3 being Nat st b1 in L~ b2 & 1 <= b3 & b3 <= width (GoB b2) holds
b1 `1 <= ((GoB b2) * (len (GoB b2)),b3) `1
proof end;

theorem Th35: :: JORDAN5D:35
for b1 being Point of (TOP-REAL 2)
for b2 being non constant standard special_circular_sequence
for b3 being Nat st b1 in L~ b2 & 1 <= b3 & b3 <= len (GoB b2) holds
((GoB b2) * b3,1) `2 <= b1 `2
proof end;

theorem Th36: :: JORDAN5D:36
for b1 being Point of (TOP-REAL 2)
for b2 being non constant standard special_circular_sequence
for b3 being Nat st b1 in L~ b2 & 1 <= b3 & b3 <= len (GoB b2) holds
b1 `2 <= ((GoB b2) * b3,(width (GoB b2))) `2
proof end;

theorem Th37: :: JORDAN5D:37
for b1 being non constant standard special_circular_sequence
for b2, b3 being Nat st 1 <= b2 & b2 <= len (GoB b1) & 1 <= b3 & b3 <= width (GoB b1) holds
ex b4 being Point of (TOP-REAL 2) st
( b4 `1 = ((GoB b1) * b2,b3) `1 & b4 in L~ b1 )
proof end;

theorem Th38: :: JORDAN5D:38
for b1 being non constant standard special_circular_sequence
for b2, b3 being Nat st 1 <= b2 & b2 <= len (GoB b1) & 1 <= b3 & b3 <= width (GoB b1) holds
ex b4 being Point of (TOP-REAL 2) st
( b4 `2 = ((GoB b1) * b2,b3) `2 & b4 in L~ b1 )
proof end;

theorem Th39: :: JORDAN5D:39
for b1 being non constant standard special_circular_sequence holds W-bound (L~ b1) = ((GoB b1) * 1,1) `1
proof end;

theorem Th40: :: JORDAN5D:40
for b1 being non constant standard special_circular_sequence holds S-bound (L~ b1) = ((GoB b1) * 1,1) `2
proof end;

theorem Th41: :: JORDAN5D:41
for b1 being non constant standard special_circular_sequence holds E-bound (L~ b1) = ((GoB b1) * (len (GoB b1)),1) `1
proof end;

theorem Th42: :: JORDAN5D:42
for b1 being non constant standard special_circular_sequence holds N-bound (L~ b1) = ((GoB b1) * 1,(width (GoB b1))) `2
proof end;

theorem Th43: :: JORDAN5D:43
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2, b3, b4 being Nat
for b5 being non empty finite Subset of NAT st 1 <= b2 & b2 <= len b1 & 1 <= b3 & b3 <= len (GoB b1) & b5 = { b6 where B is Nat : ( [b3,b6] in Indices (GoB b1) & ex b1 being Nat st
( b7 in dom b1 & b1 /. b7 = (GoB b1) * b3,b6 ) ) } & (b1 /. b2) `1 = ((GoB b1) * b3,1) `1 & b4 = min b5 holds
((GoB b1) * b3,b4) `2 <= (b1 /. b2) `2
proof end;

theorem Th44: :: JORDAN5D:44
for b1 being non constant standard special_circular_sequence
for b2, b3, b4 being Nat
for b5 being non empty finite Subset of NAT st 1 <= b2 & b2 <= len b1 & 1 <= b3 & b3 <= width (GoB b1) & b5 = { b6 where B is Nat : ( [b6,b3] in Indices (GoB b1) & ex b1 being Nat st
( b7 in dom b1 & b1 /. b7 = (GoB b1) * b6,b3 ) ) } & (b1 /. b2) `2 = ((GoB b1) * 1,b3) `2 & b4 = min b5 holds
((GoB b1) * b4,b3) `1 <= (b1 /. b2) `1
proof end;

theorem Th45: :: JORDAN5D:45
for b1 being non constant standard special_circular_sequence
for b2, b3, b4 being Nat
for b5 being non empty finite Subset of NAT st 1 <= b2 & b2 <= len b1 & 1 <= b3 & b3 <= width (GoB b1) & b5 = { b6 where B is Nat : ( [b6,b3] in Indices (GoB b1) & ex b1 being Nat st
( b7 in dom b1 & b1 /. b7 = (GoB b1) * b6,b3 ) ) } & (b1 /. b2) `2 = ((GoB b1) * 1,b3) `2 & b4 = max b5 holds
((GoB b1) * b4,b3) `1 >= (b1 /. b2) `1
proof end;

theorem Th46: :: JORDAN5D:46
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2, b3, b4 being Nat
for b5 being non empty finite Subset of NAT st 1 <= b2 & b2 <= len b1 & 1 <= b3 & b3 <= len (GoB b1) & b5 = { b6 where B is Nat : ( [b3,b6] in Indices (GoB b1) & ex b1 being Nat st
( b7 in dom b1 & b1 /. b7 = (GoB b1) * b3,b6 ) ) } & (b1 /. b2) `1 = ((GoB b1) * b3,1) `1 & b4 = max b5 holds
((GoB b1) * b3,b4) `2 >= (b1 /. b2) `2
proof end;

Lemma45: for b1 being Nat
for b2 being Point of (TOP-REAL 2)
for b3 being non empty finite Subset of NAT
for b4 being non constant standard special_circular_sequence st b2 `1 = W-bound (L~ b4) & b2 in L~ b4 & b3 = { b5 where B is Nat : ( [1,b5] in Indices (GoB b4) & ex b1 being Nat st
( b6 in dom b4 & b4 /. b6 = (GoB b4) * 1,b5 ) ) } & b1 = min b3 holds
((GoB b4) * 1,b1) `2 <= b2 `2
proof end;

Lemma46: for b1 being Nat
for b2 being Point of (TOP-REAL 2)
for b3 being non empty finite Subset of NAT
for b4 being non constant standard special_circular_sequence st b2 `1 = W-bound (L~ b4) & b2 in L~ b4 & b3 = { b5 where B is Nat : ( [1,b5] in Indices (GoB b4) & ex b1 being Nat st
( b6 in dom b4 & b4 /. b6 = (GoB b4) * 1,b5 ) ) } & b1 = max b3 holds
((GoB b4) * 1,b1) `2 >= b2 `2
proof end;

Lemma47: for b1 being Nat
for b2 being Point of (TOP-REAL 2)
for b3 being non empty finite Subset of NAT
for b4 being non constant standard special_circular_sequence st b2 `1 = E-bound (L~ b4) & b2 in L~ b4 & b3 = { b5 where B is Nat : ( [(len (GoB b4)),b5] in Indices (GoB b4) & ex b1 being Nat st
( b6 in dom b4 & b4 /. b6 = (GoB b4) * (len (GoB b4)),b5 ) ) } & b1 = min b3 holds
((GoB b4) * (len (GoB b4)),b1) `2 <= b2 `2
proof end;

Lemma48: for b1 being Nat
for b2 being Point of (TOP-REAL 2)
for b3 being non empty finite Subset of NAT
for b4 being non constant standard special_circular_sequence st b2 `1 = E-bound (L~ b4) & b2 in L~ b4 & b3 = { b5 where B is Nat : ( [(len (GoB b4)),b5] in Indices (GoB b4) & ex b1 being Nat st
( b6 in dom b4 & b4 /. b6 = (GoB b4) * (len (GoB b4)),b5 ) ) } & b1 = max b3 holds
((GoB b4) * (len (GoB b4)),b1) `2 >= b2 `2
proof end;

Lemma49: for b1 being Nat
for b2 being Point of (TOP-REAL 2)
for b3 being non empty finite Subset of NAT
for b4 being non constant standard special_circular_sequence st b2 `2 = S-bound (L~ b4) & b2 in L~ b4 & b3 = { b5 where B is Nat : ( [b5,1] in Indices (GoB b4) & ex b1 being Nat st
( b6 in dom b4 & b4 /. b6 = (GoB b4) * b5,1 ) ) } & b1 = min b3 holds
((GoB b4) * b1,1) `1 <= b2 `1
proof end;

Lemma50: for b1 being Nat
for b2 being Point of (TOP-REAL 2)
for b3 being non empty finite Subset of NAT
for b4 being non constant standard special_circular_sequence st b2 `2 = N-bound (L~ b4) & b2 in L~ b4 & b3 = { b5 where B is Nat : ( [b5,(width (GoB b4))] in Indices (GoB b4) & ex b1 being Nat st
( b6 in dom b4 & b4 /. b6 = (GoB b4) * b5,(width (GoB b4)) ) ) } & b1 = min b3 holds
((GoB b4) * b1,(width (GoB b4))) `1 <= b2 `1
proof end;

Lemma51: for b1 being non constant standard special_circular_sequence
for b2 being Nat
for b3 being Point of (TOP-REAL 2)
for b4 being non empty finite Subset of NAT st b3 `2 = S-bound (L~ b1) & b3 in L~ b1 & b4 = { b5 where B is Nat : ( [b5,1] in Indices (GoB b1) & ex b1 being Nat st
( b6 in dom b1 & b1 /. b6 = (GoB b1) * b5,1 ) ) } & b2 = max b4 holds
((GoB b1) * b2,1) `1 >= b3 `1
proof end;

Lemma52: for b1 being non constant standard special_circular_sequence
for b2 being Nat
for b3 being Point of (TOP-REAL 2)
for b4 being non empty finite Subset of NAT st b3 `2 = N-bound (L~ b1) & b3 in L~ b1 & b4 = { b5 where B is Nat : ( [b5,(width (GoB b1))] in Indices (GoB b1) & ex b1 being Nat st
( b6 in dom b1 & b1 /. b6 = (GoB b1) * b5,(width (GoB b1)) ) ) } & b2 = max b4 holds
((GoB b1) * b2,(width (GoB b1))) `1 >= b3 `1
proof end;

Lemma53: for b1 being non constant standard special_circular_sequence holds len b1 >= 2
proof end;

definition
let c1 be non constant standard special_circular_sequence;
func i_s_w c1 -> Nat means :Def1: :: JORDAN5D:def 1
( [1,a2] in Indices (GoB a1) & (GoB a1) * 1,a2 = W-min (L~ a1) );
existence
ex b1 being Nat st
( [1,b1] in Indices (GoB c1) & (GoB c1) * 1,b1 = W-min (L~ c1) )
proof end;
uniqueness
for b1, b2 being Nat st [1,b1] in Indices (GoB c1) & (GoB c1) * 1,b1 = W-min (L~ c1) & [1,b2] in Indices (GoB c1) & (GoB c1) * 1,b2 = W-min (L~ c1) holds
b1 = b2 by GOBOARD1:21;
func i_n_w c1 -> Nat means :Def2: :: JORDAN5D:def 2
( [1,a2] in Indices (GoB a1) & (GoB a1) * 1,a2 = W-max (L~ a1) );
existence
ex b1 being Nat st
( [1,b1] in Indices (GoB c1) & (GoB c1) * 1,b1 = W-max (L~ c1) )
proof end;
uniqueness
for b1, b2 being Nat st [1,b1] in Indices (GoB c1) & (GoB c1) * 1,b1 = W-max (L~ c1) & [1,b2] in Indices (GoB c1) & (GoB c1) * 1,b2 = W-max (L~ c1) holds
b1 = b2 by GOBOARD1:21;
func i_s_e c1 -> Nat means :Def3: :: JORDAN5D:def 3
( [(len (GoB a1)),a2] in Indices (GoB a1) & (GoB a1) * (len (GoB a1)),a2 = E-min (L~ a1) );
existence
ex b1 being Nat st
( [(len (GoB c1)),b1] in Indices (GoB c1) & (GoB c1) * (len (GoB c1)),b1 = E-min (L~ c1) )
proof end;
uniqueness
for b1, b2 being Nat st [(len (GoB c1)),b1] in Indices (GoB c1) & (GoB c1) * (len (GoB c1)),b1 = E-min (L~ c1) & [(len (GoB c1)),b2] in Indices (GoB c1) & (GoB c1) * (len (GoB c1)),b2 = E-min (L~ c1) holds
b1 = b2 by GOBOARD1:21;
func i_n_e c1 -> Nat means :Def4: :: JORDAN5D:def 4
( [(len (GoB a1)),a2] in Indices (GoB a1) & (GoB a1) * (len (GoB a1)),a2 = E-max (L~ a1) );
existence
ex b1 being Nat st
( [(len (GoB c1)),b1] in Indices (GoB c1) & (GoB c1) * (len (GoB c1)),b1 = E-max (L~ c1) )
proof end;
uniqueness
for b1, b2 being Nat st [(len (GoB c1)),b1] in Indices (GoB c1) & (GoB c1) * (len (GoB c1)),b1 = E-max (L~ c1) & [(len (GoB c1)),b2] in Indices (GoB c1) & (GoB c1) * (len (GoB c1)),b2 = E-max (L~ c1) holds
b1 = b2 by GOBOARD1:21;
func i_w_s c1 -> Nat means :Def5: :: JORDAN5D:def 5
( [a2,1] in Indices (GoB a1) & (GoB a1) * a2,1 = S-min (L~ a1) );
existence
ex b1 being Nat st
( [b1,1] in Indices (GoB c1) & (GoB c1) * b1,1 = S-min (L~ c1) )
proof end;
uniqueness
for b1, b2 being Nat st [b1,1] in Indices (GoB c1) & (GoB c1) * b1,1 = S-min (L~ c1) & [b2,1] in Indices (GoB c1) & (GoB c1) * b2,1 = S-min (L~ c1) holds
b1 = b2 by GOBOARD1:21;
func i_e_s c1 -> Nat means :Def6: :: JORDAN5D:def 6
( [a2,1] in Indices (GoB a1) & (GoB a1) * a2,1 = S-max (L~ a1) );
existence
ex b1 being Nat st
( [b1,1] in Indices (GoB c1) & (GoB c1) * b1,1 = S-max (L~ c1) )
proof end;
uniqueness
for b1, b2 being Nat st [b1,1] in Indices (GoB c1) & (GoB c1) * b1,1 = S-max (L~ c1) & [b2,1] in Indices (GoB c1) & (GoB c1) * b2,1 = S-max (L~ c1) holds
b1 = b2 by GOBOARD1:21;
func i_w_n c1 -> Nat means :Def7: :: JORDAN5D:def 7
( [a2,(width (GoB a1))] in Indices (GoB a1) & (GoB a1) * a2,(width (GoB a1)) = N-min (L~ a1) );
existence
ex b1 being Nat st
( [b1,(width (GoB c1))] in Indices (GoB c1) & (GoB c1) * b1,(width (GoB c1)) = N-min (L~ c1) )
proof end;
uniqueness
for b1, b2 being Nat st [b1,(width (GoB c1))] in Indices (GoB c1) & (GoB c1) * b1,(width (GoB c1)) = N-min (L~ c1) & [b2,(width (GoB c1))] in Indices (GoB c1) & (GoB c1) * b2,(width (GoB c1)) = N-min (L~ c1) holds
b1 = b2 by GOBOARD1:21;
func i_e_n c1 -> Nat means :Def8: :: JORDAN5D:def 8
( [a2,(width (GoB a1))] in Indices (GoB a1) & (GoB a1) * a2,(width (GoB a1)) = N-max (L~ a1) );
existence
ex b1 being Nat st
( [b1,(width (GoB c1))] in Indices (GoB c1) & (GoB c1) * b1,(width (GoB c1)) = N-max (L~ c1) )
proof end;
uniqueness
for b1, b2 being Nat st [b1,(width (GoB c1))] in Indices (GoB c1) & (GoB c1) * b1,(width (GoB c1)) = N-max (L~ c1) & [b2,(width (GoB c1))] in Indices (GoB c1) & (GoB c1) * b2,(width (GoB c1)) = N-max (L~ c1) holds
b1 = b2 by GOBOARD1:21;
end;

:: deftheorem Def1 defines i_s_w JORDAN5D:def 1 :
for b1 being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = i_s_w b1 iff ( [1,b2] in Indices (GoB b1) & (GoB b1) * 1,b2 = W-min (L~ b1) ) );

:: deftheorem Def2 defines i_n_w JORDAN5D:def 2 :
for b1 being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = i_n_w b1 iff ( [1,b2] in Indices (GoB b1) & (GoB b1) * 1,b2 = W-max (L~ b1) ) );

:: deftheorem Def3 defines i_s_e JORDAN5D:def 3 :
for b1 being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = i_s_e b1 iff ( [(len (GoB b1)),b2] in Indices (GoB b1) & (GoB b1) * (len (GoB b1)),b2 = E-min (L~ b1) ) );

:: deftheorem Def4 defines i_n_e JORDAN5D:def 4 :
for b1 being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = i_n_e b1 iff ( [(len (GoB b1)),b2] in Indices (GoB b1) & (GoB b1) * (len (GoB b1)),b2 = E-max (L~ b1) ) );

:: deftheorem Def5 defines i_w_s JORDAN5D:def 5 :
for b1 being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = i_w_s b1 iff ( [b2,1] in Indices (GoB b1) & (GoB b1) * b2,1 = S-min (L~ b1) ) );

:: deftheorem Def6 defines i_e_s JORDAN5D:def 6 :
for b1 being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = i_e_s b1 iff ( [b2,1] in Indices (GoB b1) & (GoB b1) * b2,1 = S-max (L~ b1) ) );

:: deftheorem Def7 defines i_w_n JORDAN5D:def 7 :
for b1 being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = i_w_n b1 iff ( [b2,(width (GoB b1))] in Indices (GoB b1) & (GoB b1) * b2,(width (GoB b1)) = N-min (L~ b1) ) );

:: deftheorem Def8 defines i_e_n JORDAN5D:def 8 :
for b1 being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = i_e_n b1 iff ( [b2,(width (GoB b1))] in Indices (GoB b1) & (GoB b1) * b2,(width (GoB b1)) = N-max (L~ b1) ) );

theorem Th47: :: JORDAN5D:47
for b1 being non constant standard special_circular_sequence holds
( 1 <= i_w_n b1 & i_w_n b1 <= len (GoB b1) & 1 <= i_e_n b1 & i_e_n b1 <= len (GoB b1) & 1 <= i_w_s b1 & i_w_s b1 <= len (GoB b1) & 1 <= i_e_s b1 & i_e_s b1 <= len (GoB b1) )
proof end;

theorem Th48: :: JORDAN5D:48
for b1 being non constant standard special_circular_sequence holds
( 1 <= i_n_e b1 & i_n_e b1 <= width (GoB b1) & 1 <= i_s_e b1 & i_s_e b1 <= width (GoB b1) & 1 <= i_n_w b1 & i_n_w b1 <= width (GoB b1) & 1 <= i_s_w b1 & i_s_w b1 <= width (GoB b1) )
proof end;

Lemma62: for b1 being non constant standard special_circular_sequence
for b2, b3 being Nat st 1 <= b2 & b2 + 1 <= len b1 & 1 <= b3 & b3 + 1 <= len b1 & b1 . b2 = b1 . b3 holds
b2 = b3
proof end;

definition
let c1 be non constant standard special_circular_sequence;
func n_s_w c1 -> Nat means :Def9: :: JORDAN5D:def 9
( 1 <= a2 & a2 + 1 <= len a1 & a1 . a2 = W-min (L~ a1) );
existence
ex b1 being Nat st
( 1 <= b1 & b1 + 1 <= len c1 & c1 . b1 = W-min (L~ c1) )
proof end;
uniqueness
for b1, b2 being Nat st 1 <= b1 & b1 + 1 <= len c1 & c1 . b1 = W-min (L~ c1) & 1 <= b2 & b2 + 1 <= len c1 & c1 . b2 = W-min (L~ c1) holds
b1 = b2 by Lemma62;
func n_n_w c1 -> Nat means :Def10: :: JORDAN5D:def 10
( 1 <= a2 & a2 + 1 <= len a1 & a1 . a2 = W-max (L~ a1) );
existence
ex b1 being Nat st
( 1 <= b1 & b1 + 1 <= len c1 & c1 . b1 = W-max (L~ c1) )
proof end;
uniqueness
for b1, b2 being Nat st 1 <= b1 & b1 + 1 <= len c1 & c1 . b1 = W-max (L~ c1) & 1 <= b2 & b2 + 1 <= len c1 & c1 . b2 = W-max (L~ c1) holds
b1 = b2 by Lemma62;
func n_s_e c1 -> Nat means :Def11: :: JORDAN5D:def 11
( 1 <= a2 & a2 + 1 <= len a1 & a1 . a2 = E-min (L~ a1) );
existence
ex b1 being Nat st
( 1 <= b1 & b1 + 1 <= len c1 & c1 . b1 = E-min (L~ c1) )
proof end;
uniqueness
for b1, b2 being Nat st 1 <= b1 & b1 + 1 <= len c1 & c1 . b1 = E-min (L~ c1) & 1 <= b2 & b2 + 1 <= len c1 & c1 . b2 = E-min (L~ c1) holds
b1 = b2 by Lemma62;
func n_n_e c1 -> Nat means :Def12: :: JORDAN5D:def 12
( 1 <= a2 & a2 + 1 <= len a1 & a1 . a2 = E-max (L~ a1) );
existence
ex b1 being Nat st
( 1 <= b1 & b1 + 1 <= len c1 & c1 . b1 = E-max (L~ c1) )
proof end;
uniqueness
for b1, b2 being Nat st 1 <= b1 & b1 + 1 <= len c1 & c1 . b1 = E-max (L~ c1) & 1 <= b2 & b2 + 1 <= len c1 & c1 . b2 = E-max (L~ c1) holds
b1 = b2 by Lemma62;
func n_w_s c1 -> Nat means :Def13: :: JORDAN5D:def 13
( 1 <= a2 & a2 + 1 <= len a1 & a1 . a2 = S-min (L~ a1) );
existence
ex b1 being Nat st
( 1 <= b1 & b1 + 1 <= len c1 & c1 . b1 = S-min (L~ c1) )
proof end;
uniqueness
for b1, b2 being Nat st 1 <= b1 & b1 + 1 <= len c1 & c1 . b1 = S-min (L~ c1) & 1 <= b2 & b2 + 1 <= len c1 & c1 . b2 = S-min (L~ c1) holds
b1 = b2 by Lemma62;
func n_e_s c1 -> Nat means :Def14: :: JORDAN5D:def 14
( 1 <= a2 & a2 + 1 <= len a1 & a1 . a2 = S-max (L~ a1) );
existence
ex b1 being Nat st
( 1 <= b1 & b1 + 1 <= len c1 & c1 . b1 = S-max (L~ c1) )
proof end;
uniqueness
for b1, b2 being Nat st 1 <= b1 & b1 + 1 <= len c1 & c1 . b1 = S-max (L~ c1) & 1 <= b2 & b2 + 1 <= len c1 & c1 . b2 = S-max (L~ c1) holds
b1 = b2 by Lemma62;
func n_w_n c1 -> Nat means :Def15: :: JORDAN5D:def 15
( 1 <= a2 & a2 + 1 <= len a1 & a1 . a2 = N-min (L~ a1) );
existence
ex b1 being Nat st
( 1 <= b1 & b1 + 1 <= len c1 & c1 . b1 = N-min (L~ c1) )
proof end;
uniqueness
for b1, b2 being Nat st 1 <= b1 & b1 + 1 <= len c1 & c1 . b1 = N-min (L~ c1) & 1 <= b2 & b2 + 1 <= len c1 & c1 . b2 = N-min (L~ c1) holds
b1 = b2 by Lemma62;
func n_e_n c1 -> Nat means :Def16: :: JORDAN5D:def 16
( 1 <= a2 & a2 + 1 <= len a1 & a1 . a2 = N-max (L~ a1) );
existence
ex b1 being Nat st
( 1 <= b1 & b1 + 1 <= len c1 & c1 . b1 = N-max (L~ c1) )
proof end;
uniqueness
for b1, b2 being Nat st 1 <= b1 & b1 + 1 <= len c1 & c1 . b1 = N-max (L~ c1) & 1 <= b2 & b2 + 1 <= len c1 & c1 . b2 = N-max (L~ c1) holds
b1 = b2 by Lemma62;
end;

:: deftheorem Def9 defines n_s_w JORDAN5D:def 9 :
for b1 being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = n_s_w b1 iff ( 1 <= b2 & b2 + 1 <= len b1 & b1 . b2 = W-min (L~ b1) ) );

:: deftheorem Def10 defines n_n_w JORDAN5D:def 10 :
for b1 being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = n_n_w b1 iff ( 1 <= b2 & b2 + 1 <= len b1 & b1 . b2 = W-max (L~ b1) ) );

:: deftheorem Def11 defines n_s_e JORDAN5D:def 11 :
for b1 being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = n_s_e b1 iff ( 1 <= b2 & b2 + 1 <= len b1 & b1 . b2 = E-min (L~ b1) ) );

:: deftheorem Def12 defines n_n_e JORDAN5D:def 12 :
for b1 being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = n_n_e b1 iff ( 1 <= b2 & b2 + 1 <= len b1 & b1 . b2 = E-max (L~ b1) ) );

:: deftheorem Def13 defines n_w_s JORDAN5D:def 13 :
for b1 being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = n_w_s b1 iff ( 1 <= b2 & b2 + 1 <= len b1 & b1 . b2 = S-min (L~ b1) ) );

:: deftheorem Def14 defines n_e_s JORDAN5D:def 14 :
for b1 being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = n_e_s b1 iff ( 1 <= b2 & b2 + 1 <= len b1 & b1 . b2 = S-max (L~ b1) ) );

:: deftheorem Def15 defines n_w_n JORDAN5D:def 15 :
for b1 being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = n_w_n b1 iff ( 1 <= b2 & b2 + 1 <= len b1 & b1 . b2 = N-min (L~ b1) ) );

:: deftheorem Def16 defines n_e_n JORDAN5D:def 16 :
for b1 being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = n_e_n b1 iff ( 1 <= b2 & b2 + 1 <= len b1 & b1 . b2 = N-max (L~ b1) ) );

theorem Th49: :: JORDAN5D:49
for b1 being non constant standard special_circular_sequence holds n_w_n b1 <> n_w_s b1
proof end;

theorem Th50: :: JORDAN5D:50
for b1 being non constant standard special_circular_sequence holds n_s_w b1 <> n_s_e b1
proof end;

theorem Th51: :: JORDAN5D:51
for b1 being non constant standard special_circular_sequence holds n_e_n b1 <> n_e_s b1
proof end;

theorem Th52: :: JORDAN5D:52
for b1 being non constant standard special_circular_sequence holds n_n_w b1 <> n_n_e b1
proof end;