:: JORDAN1H semantic presentation

registration
cluster with_non-empty_element set ;
existence
ex b1 being set st b1 is with_non-empty_element
proof end;
end;

registration
let c1 be non empty with_non-empty_element set ;
cluster non empty non-empty FinSequence of a1 * ;
existence
ex b1 being FinSequence of c1 * st
( not b1 is empty & b1 is non-empty )
proof end;
end;

registration
let c1 be non empty with_non-empty_elements set ;
cluster non empty non-empty FinSequence of a1 * ;
existence
ex b1 being FinSequence of c1 * st
( not b1 is empty & b1 is non-empty )
proof end;
end;

registration
let c1 be non-empty Function-yielding Function;
cluster rngs a1 -> non-empty ;
coherence
rngs c1 is non-empty
proof end;
end;

theorem Th1: :: JORDAN1H:1
canceled;

theorem Th2: :: JORDAN1H:2
canceled;

theorem Th3: :: JORDAN1H:3
canceled;

theorem Th4: :: JORDAN1H:4
for b1, b2 being Point of (TOP-REAL 2) holds (LSeg b1,b2) \ {b1,b2} is convex
proof end;

theorem Th5: :: JORDAN1H:5
for b1, b2 being Point of (TOP-REAL 2) holds (LSeg b1,b2) \ {b1,b2} is connected
proof end;

theorem Th6: :: JORDAN1H:6
for b1, b2 being Point of (TOP-REAL 2) st b1 <> b2 holds
b1 in Cl ((LSeg b1,b2) \ {b1,b2})
proof end;

theorem Th7: :: JORDAN1H:7
for b1, b2 being Point of (TOP-REAL 2) st b1 <> b2 holds
Cl ((LSeg b1,b2) \ {b1,b2}) = LSeg b1,b2
proof end;

theorem Th8: :: JORDAN1H:8
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b2 <> b3 & (LSeg b2,b3) \ {b2,b3} c= b1 holds
LSeg b2,b3 c= Cl b1
proof end;

definition
func RealOrd -> Relation of REAL equals :: JORDAN1H:def 1
{ [b1,b2] where B is Real, B is Real : b1 <= b2 } ;
coherence
{ [b1,b2] where B is Real, B is Real : b1 <= b2 } is Relation of REAL
proof end;
end;

:: deftheorem Def1 defines RealOrd JORDAN1H:def 1 :
RealOrd = { [b1,b2] where B is Real, B is Real : b1 <= b2 } ;

theorem Th9: :: JORDAN1H:9
for b1, b2 being Real st [b1,b2] in RealOrd holds
b1 <= b2
proof end;

Lemma5: RealOrd is_reflexive_in REAL
proof end;

Lemma6: RealOrd is_antisymmetric_in REAL
proof end;

Lemma7: RealOrd is_transitive_in REAL
proof end;

Lemma8: RealOrd is_connected_in REAL
proof end;

theorem Th10: :: JORDAN1H:10
field RealOrd = REAL
proof end;

registration
cluster RealOrd -> reflexive antisymmetric transitive total being_linear-order ;
coherence
( RealOrd is total & RealOrd is reflexive & RealOrd is antisymmetric & RealOrd is transitive & RealOrd is being_linear-order )
proof end;
end;

theorem Th11: :: JORDAN1H:11
RealOrd linearly_orders REAL
proof end;

theorem Th12: :: JORDAN1H:12
for b1 being finite Subset of REAL holds SgmX RealOrd ,b1 is increasing
proof end;

theorem Th13: :: JORDAN1H:13
for b1 being FinSequence of REAL
for b2 being finite Subset of REAL st b2 = rng b1 holds
SgmX RealOrd ,b2 = Incr b1
proof end;

registration
let c1 be finite Subset of REAL ;
cluster SgmX RealOrd ,a1 -> increasing ;
coherence
SgmX RealOrd ,c1 is increasing by Th12;
end;

theorem Th14: :: JORDAN1H:14
canceled;

theorem Th15: :: JORDAN1H:15
for b1 being non empty set
for b2 being finite Subset of b1
for b3 being being_linear-order Order of b1 holds len (SgmX b3,b2) = card b2
proof end;

theorem Th16: :: JORDAN1H:16
for b1 being FinSequence of (TOP-REAL 2) holds X_axis b1 = proj1 * b1
proof end;

theorem Th17: :: JORDAN1H:17
for b1 being FinSequence of (TOP-REAL 2) holds Y_axis b1 = proj2 * b1
proof end;

definition
let c1 be non empty set ;
let c2 be FinSequence of c1 * ;
redefine func Values as Values c2 -> Subset of a1;
coherence
Values c2 is Subset of c1
proof end;
end;

registration
let c1 be non empty with_non-empty_elements set ;
let c2 be non empty non-empty FinSequence of c1 * ;
cluster Values a2 -> non empty ;
coherence
not Values c2 is empty
proof end;
end;

theorem Th18: :: JORDAN1H:18
for b1 being non empty set
for b2 being Matrix of b1
for b3 being Nat st b3 in Seg (width b2) holds
rng (Col b2,b3) c= Values b2
proof end;

theorem Th19: :: JORDAN1H:19
for b1 being non empty set
for b2 being Matrix of b1
for b3 being Nat st b3 in dom b2 holds
rng (Line b2,b3) c= Values b2
proof end;

theorem Th20: :: JORDAN1H:20
for b1 being V4 X_increasing-in-column Matrix of (TOP-REAL 2) holds len b1 <= card (proj1 .: (Values b1))
proof end;

theorem Th21: :: JORDAN1H:21
for b1 being X_equal-in-line Matrix of (TOP-REAL 2) holds card (proj1 .: (Values b1)) <= len b1
proof end;

theorem Th22: :: JORDAN1H:22
for b1 being V4 X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2) holds len b1 = card (proj1 .: (Values b1))
proof end;

theorem Th23: :: JORDAN1H:23
for b1 being V4 Y_increasing-in-line Matrix of (TOP-REAL 2) holds width b1 <= card (proj2 .: (Values b1))
proof end;

theorem Th24: :: JORDAN1H:24
for b1 being V4 Y_equal-in-column Matrix of (TOP-REAL 2) holds card (proj2 .: (Values b1)) <= width b1
proof end;

theorem Th25: :: JORDAN1H:25
for b1 being V4 Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2) holds width b1 = card (proj2 .: (Values b1))
proof end;

theorem Th26: :: JORDAN1H:26
for b1 being Go-board
for b2 being FinSequence of (TOP-REAL 2) st b2 is_sequence_on b1 holds
for b3 being Nat st 1 <= b3 & b3 + 1 <= len b2 holds
LSeg b2,b3 c= left_cell b2,b3,b1
proof end;

theorem Th27: :: JORDAN1H:27
for b1 being Nat
for b2 being standard special_circular_sequence st 1 <= b1 & b1 + 1 <= len b2 holds
left_cell b2,b1,(GoB b2) = left_cell b2,b1
proof end;

theorem Th28: :: JORDAN1H:28
for b1 being Go-board
for b2 being FinSequence of (TOP-REAL 2) st b2 is_sequence_on b1 holds
for b3 being Nat st 1 <= b3 & b3 + 1 <= len b2 holds
LSeg b2,b3 c= right_cell b2,b3,b1
proof end;

theorem Th29: :: JORDAN1H:29
for b1 being Nat
for b2 being standard special_circular_sequence st 1 <= b1 & b1 + 1 <= len b2 holds
right_cell b2,b1,(GoB b2) = right_cell b2,b1
proof end;

theorem Th30: :: JORDAN1H:30
for b1 being Subset of (TOP-REAL 2)
for b2 being non constant standard special_circular_sequence holds
( not b1 is_a_component_of (L~ b2) ` or b1 = RightComp b2 or b1 = LeftComp b2 )
proof end;

theorem Th31: :: JORDAN1H:31
for b1 being Go-board
for b2 being non constant standard special_circular_sequence st b2 is_sequence_on b1 holds
for b3 being Nat st 1 <= b3 & b3 + 1 <= len b2 holds
( Int (right_cell b2,b3,b1) c= RightComp b2 & Int (left_cell b2,b3,b1) c= LeftComp b2 )
proof end;

theorem Th32: :: JORDAN1H:32
for b1, b2, b3, b4 being Nat
for b5 being Go-board st [b1,b2] in Indices b5 & [b3,b4] in Indices b5 & b5 * b1,b2 = b5 * b3,b4 holds
( b1 = b3 & b2 = b4 )
proof end;

theorem Th33: :: JORDAN1H:33
for b1, b2 being Nat
for b3 being FinSequence of (TOP-REAL 2)
for b4 being Go-board st b3 is_sequence_on b4 holds
mid b3,b1,b2 is_sequence_on b4
proof end;

registration
cluster -> non empty non-empty FinSequence of the carrier of (TOP-REAL 2) * ;
coherence
for b1 being Go-board holds
( not b1 is empty & b1 is non-empty )
proof end;
end;

theorem Th34: :: JORDAN1H:34
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 <= len b2 holds
(SgmX RealOrd ,(proj1 .: (Values b2))) . b1 = (b2 * b1,1) `1
proof end;

theorem Th35: :: JORDAN1H:35
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 <= width b2 holds
(SgmX RealOrd ,(proj2 .: (Values b2))) . b1 = (b2 * 1,b1) `2
proof end;

theorem Th36: :: JORDAN1H:36
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2 being Go-board st b1 is_sequence_on b2 & ex b3 being Nat st
( [1,b3] in Indices b2 & b2 * 1,b3 in rng b1 ) & ex b3 being Nat st
( [(len b2),b3] in Indices b2 & b2 * (len b2),b3 in rng b1 ) holds
proj1 .: (rng b1) = proj1 .: (Values b2)
proof end;

theorem Th37: :: JORDAN1H:37
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2 being Go-board st b1 is_sequence_on b2 & ex b3 being Nat st
( [b3,1] in Indices b2 & b2 * b3,1 in rng b1 ) & ex b3 being Nat st
( [b3,(width b2)] in Indices b2 & b2 * b3,(width b2) in rng b1 ) holds
proj2 .: (rng b1) = proj2 .: (Values b2)
proof end;

registration
let c1 be Go-board;
cluster Values a1 -> non empty ;
coherence
not Values c1 is empty
proof end;
end;

theorem Th38: :: JORDAN1H:38
for b1 being Go-board holds b1 = GoB (SgmX RealOrd ,(proj1 .: (Values b1))),(SgmX RealOrd ,(proj2 .: (Values b1)))
proof end;

theorem Th39: :: JORDAN1H:39
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2 being Go-board st proj1 .: (rng b1) = proj1 .: (Values b2) & proj2 .: (rng b1) = proj2 .: (Values b2) holds
b2 = GoB b1
proof end;

theorem Th40: :: JORDAN1H:40
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2 being Go-board st b1 is_sequence_on b2 & ex b3 being Nat st
( [1,b3] in Indices b2 & b2 * 1,b3 in rng b1 ) & ex b3 being Nat st
( [b3,1] in Indices b2 & b2 * b3,1 in rng b1 ) & ex b3 being Nat st
( [(len b2),b3] in Indices b2 & b2 * (len b2),b3 in rng b1 ) & ex b3 being Nat st
( [b3,(width b2)] in Indices b2 & b2 * b3,(width b2) in rng b1 ) holds
b2 = GoB b1
proof end;

theorem Th41: :: JORDAN1H:41
for b1, b2, b3 being Nat
for b4 being compact non horizontal non vertical Subset of (TOP-REAL 2) st b1 <= b2 & 1 <= b3 & b3 + 1 <= len (Gauge b4,b2) holds
[\(((b3 - 2) / (2 |^ (b2 -' b1))) + 2)/] is Nat
proof end;

theorem Th42: :: JORDAN1H:42
for b1, b2, b3 being Nat
for b4 being compact non horizontal non vertical Subset of (TOP-REAL 2) st b1 <= b2 & 1 <= b3 & b3 + 1 <= len (Gauge b4,b2) holds
( 1 <= [\(((b3 - 2) / (2 |^ (b2 -' b1))) + 2)/] & [\(((b3 - 2) / (2 |^ (b2 -' b1))) + 2)/] + 1 <= len (Gauge b4,b1) )
proof end;

theorem Th43: :: JORDAN1H:43
for b1, b2, b3, b4 being Nat
for b5 being compact non horizontal non vertical Subset of (TOP-REAL 2) st b1 <= b2 & 1 <= b3 & b3 + 1 <= len (Gauge b5,b2) & 1 <= b4 & b4 + 1 <= width (Gauge b5,b2) holds
ex b6, b7 being Nat st
( b6 = [\(((b3 - 2) / (2 |^ (b2 -' b1))) + 2)/] & b7 = [\(((b4 - 2) / (2 |^ (b2 -' b1))) + 2)/] & cell (Gauge b5,b2),b3,b4 c= cell (Gauge b5,b1),b6,b7 )
proof end;

theorem Th44: :: JORDAN1H:44
for b1, b2, b3, b4 being Nat
for b5 being compact non horizontal non vertical Subset of (TOP-REAL 2) st b1 <= b2 & 1 <= b3 & b3 + 1 <= len (Gauge b5,b2) & 1 <= b4 & b4 + 1 <= width (Gauge b5,b2) holds
ex b6, b7 being Nat st
( 1 <= b6 & b6 + 1 <= len (Gauge b5,b1) & 1 <= b7 & b7 + 1 <= width (Gauge b5,b1) & cell (Gauge b5,b2),b3,b4 c= cell (Gauge b5,b1),b6,b7 )
proof end;

theorem Th45: :: JORDAN1H:45
canceled;

theorem Th46: :: JORDAN1H:46
canceled;

theorem Th47: :: JORDAN1H:47
for b1 being Subset of (TOP-REAL 2) st b1 is Bounded holds
not UBD b1 is Bounded
proof end;

theorem Th48: :: JORDAN1H:48
for b1 being Point of (TOP-REAL 2)
for b2 being non constant standard special_circular_sequence st Rotate b2,b1 is clockwise_oriented holds
b2 is clockwise_oriented
proof end;

theorem Th49: :: JORDAN1H:49
for b1 being non constant standard special_circular_sequence st LeftComp b1 = UBD (L~ b1) holds
b1 is clockwise_oriented
proof end;

theorem Th50: :: JORDAN1H:50
for b1 being non constant standard special_circular_sequence holds (Cl (LeftComp b1)) ` = RightComp b1
proof end;

theorem Th51: :: JORDAN1H:51
for b1 being non constant standard special_circular_sequence holds (Cl (RightComp b1)) ` = LeftComp b1
proof end;

theorem Th52: :: JORDAN1H:52
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) st b2 is connected holds
GoB (Cage b2,b1) = Gauge b2,b1
proof end;

theorem Th53: :: JORDAN1H:53
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) st b2 is connected holds
N-min b2 in right_cell (Cage b2,b1),1
proof end;

theorem Th54: :: JORDAN1H:54
for b1, b2 being Nat
for b3 being compact non horizontal non vertical Subset of (TOP-REAL 2) st b3 is connected & b1 <= b2 holds
L~ (Cage b3,b2) c= Cl (RightComp (Cage b3,b1))
proof end;

theorem Th55: :: JORDAN1H:55
for b1, b2 being Nat
for b3 being compact non horizontal non vertical Subset of (TOP-REAL 2) st b3 is connected & b1 <= b2 holds
LeftComp (Cage b3,b1) c= LeftComp (Cage b3,b2)
proof end;

theorem Th56: :: JORDAN1H:56
for b1, b2 being Nat
for b3 being compact non horizontal non vertical Subset of (TOP-REAL 2) st b3 is connected & b1 <= b2 holds
RightComp (Cage b3,b2) c= RightComp (Cage b3,b1)
proof end;

definition
let c1 be compact non horizontal non vertical Subset of (TOP-REAL 2);
let c2 be Nat;
func X-SpanStart c1,c2 -> Nat equals :: JORDAN1H:def 2
(2 |^ (a2 -' 1)) + 2;
correctness
coherence
(2 |^ (c2 -' 1)) + 2 is Nat;
;
end;

:: deftheorem Def2 defines X-SpanStart JORDAN1H:def 2 :
for b1 being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat holds X-SpanStart b1,b2 = (2 |^ (b2 -' 1)) + 2;

theorem Th57: :: JORDAN1H:57
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds X-SpanStart b2,b1 = Center (Gauge b2,b1) by JORDAN1B:17;

theorem Th58: :: JORDAN1H:58
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( 2 < X-SpanStart b2,b1 & X-SpanStart b2,b1 < len (Gauge b2,b1) )
proof end;

theorem Th59: :: JORDAN1H:59
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( 1 <= (X-SpanStart b2,b1) -' 1 & (X-SpanStart b2,b1) -' 1 < len (Gauge b2,b1) )
proof end;

definition
let c1 be compact non horizontal non vertical Subset of (TOP-REAL 2);
let c2 be Nat;
pred c2 is_sufficiently_large_for c1 means :Def3: :: JORDAN1H:def 3
ex b1 being Nat st
( b1 < width (Gauge a1,a2) & cell (Gauge a1,a2),((X-SpanStart a1,a2) -' 1),b1 c= BDD a1 );
end;

:: deftheorem Def3 defines is_sufficiently_large_for JORDAN1H:def 3 :
for b1 being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat holds
( b2 is_sufficiently_large_for b1 iff ex b3 being Nat st
( b3 < width (Gauge b1,b2) & cell (Gauge b1,b2),((X-SpanStart b1,b2) -' 1),b3 c= BDD b1 ) );

theorem Th60: :: JORDAN1H:60
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) st b1 is_sufficiently_large_for b2 holds
b1 >= 1
proof end;

theorem Th61: :: JORDAN1H:61
for b1 being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat
for b3 being FinSequence of (TOP-REAL 2) st b3 is_sequence_on Gauge b1,b2 & len b3 > 1 holds
for b4, b5 being Nat st left_cell b3,((len b3) -' 1),(Gauge b1,b2) meets b1 & [b4,b5] in Indices (Gauge b1,b2) & b3 /. ((len b3) -' 1) = (Gauge b1,b2) * b4,b5 & [b4,(b5 + 1)] in Indices (Gauge b1,b2) & b3 /. (len b3) = (Gauge b1,b2) * b4,(b5 + 1) holds
[(b4 -' 1),(b5 + 1)] in Indices (Gauge b1,b2)
proof end;

theorem Th62: :: JORDAN1H:62
for b1 being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat
for b3 being FinSequence of (TOP-REAL 2) st b3 is_sequence_on Gauge b1,b2 & len b3 > 1 holds
for b4, b5 being Nat st left_cell b3,((len b3) -' 1),(Gauge b1,b2) meets b1 & [b4,b5] in Indices (Gauge b1,b2) & b3 /. ((len b3) -' 1) = (Gauge b1,b2) * b4,b5 & [(b4 + 1),b5] in Indices (Gauge b1,b2) & b3 /. (len b3) = (Gauge b1,b2) * (b4 + 1),b5 holds
[(b4 + 1),(b5 + 1)] in Indices (Gauge b1,b2)
proof end;

theorem Th63: :: JORDAN1H:63
for b1 being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat
for b3 being FinSequence of (TOP-REAL 2) st b3 is_sequence_on Gauge b1,b2 & len b3 > 1 holds
for b4, b5 being Nat st left_cell b3,((len b3) -' 1),(Gauge b1,b2) meets b1 & [(b5 + 1),b4] in Indices (Gauge b1,b2) & b3 /. ((len b3) -' 1) = (Gauge b1,b2) * (b5 + 1),b4 & [b5,b4] in Indices (Gauge b1,b2) & b3 /. (len b3) = (Gauge b1,b2) * b5,b4 holds
[b5,(b4 -' 1)] in Indices (Gauge b1,b2)
proof end;

theorem Th64: :: JORDAN1H:64
for b1 being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat
for b3 being FinSequence of (TOP-REAL 2) st b3 is_sequence_on Gauge b1,b2 & len b3 > 1 holds
for b4, b5 being Nat st left_cell b3,((len b3) -' 1),(Gauge b1,b2) meets b1 & [b4,(b5 + 1)] in Indices (Gauge b1,b2) & b3 /. ((len b3) -' 1) = (Gauge b1,b2) * b4,(b5 + 1) & [b4,b5] in Indices (Gauge b1,b2) & b3 /. (len b3) = (Gauge b1,b2) * b4,b5 holds
[(b4 + 1),b5] in Indices (Gauge b1,b2)
proof end;

theorem Th65: :: JORDAN1H:65
for b1 being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat
for b3 being FinSequence of (TOP-REAL 2) st b3 is_sequence_on Gauge b1,b2 & len b3 > 1 holds
for b4, b5 being Nat st front_left_cell b3,((len b3) -' 1),(Gauge b1,b2) meets b1 & [b4,b5] in Indices (Gauge b1,b2) & b3 /. ((len b3) -' 1) = (Gauge b1,b2) * b4,b5 & [b4,(b5 + 1)] in Indices (Gauge b1,b2) & b3 /. (len b3) = (Gauge b1,b2) * b4,(b5 + 1) holds
[b4,(b5 + 2)] in Indices (Gauge b1,b2)
proof end;

theorem Th66: :: JORDAN1H:66
for b1 being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat
for b3 being FinSequence of (TOP-REAL 2) st b3 is_sequence_on Gauge b1,b2 & len b3 > 1 holds
for b4, b5 being Nat st front_left_cell b3,((len b3) -' 1),(Gauge b1,b2) meets b1 & [b4,b5] in Indices (Gauge b1,b2) & b3 /. ((len b3) -' 1) = (Gauge b1,b2) * b4,b5 & [(b4 + 1),b5] in Indices (Gauge b1,b2) & b3 /. (len b3) = (Gauge b1,b2) * (b4 + 1),b5 holds
[(b4 + 2),b5] in Indices (Gauge b1,b2)
proof end;

theorem Th67: :: JORDAN1H:67
for b1 being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat
for b3 being FinSequence of (TOP-REAL 2) st b3 is_sequence_on Gauge b1,b2 & len b3 > 1 holds
for b4, b5 being Nat st front_left_cell b3,((len b3) -' 1),(Gauge b1,b2) meets b1 & [(b5 + 1),b4] in Indices (Gauge b1,b2) & b3 /. ((len b3) -' 1) = (Gauge b1,b2) * (b5 + 1),b4 & [b5,b4] in Indices (Gauge b1,b2) & b3 /. (len b3) = (Gauge b1,b2) * b5,b4 holds
[(b5 -' 1),b4] in Indices (Gauge b1,b2)
proof end;

theorem Th68: :: JORDAN1H:68
for b1 being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat
for b3 being FinSequence of (TOP-REAL 2) st b3 is_sequence_on Gauge b1,b2 & len b3 > 1 holds
for b4, b5 being Nat st front_left_cell b3,((len b3) -' 1),(Gauge b1,b2) meets b1 & [b4,(b5 + 1)] in Indices (Gauge b1,b2) & b3 /. ((len b3) -' 1) = (Gauge b1,b2) * b4,(b5 + 1) & [b4,b5] in Indices (Gauge b1,b2) & b3 /. (len b3) = (Gauge b1,b2) * b4,b5 holds
[b4,(b5 -' 1)] in Indices (Gauge b1,b2)
proof end;

theorem Th69: :: JORDAN1H:69
for b1 being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat
for b3 being FinSequence of (TOP-REAL 2) st b3 is_sequence_on Gauge b1,b2 & len b3 > 1 holds
for b4, b5 being Nat st front_right_cell b3,((len b3) -' 1),(Gauge b1,b2) meets b1 & [b4,b5] in Indices (Gauge b1,b2) & b3 /. ((len b3) -' 1) = (Gauge b1,b2) * b4,b5 & [b4,(b5 + 1)] in Indices (Gauge b1,b2) & b3 /. (len b3) = (Gauge b1,b2) * b4,(b5 + 1) holds
[(b4 + 1),(b5 + 1)] in Indices (Gauge b1,b2)
proof end;

theorem Th70: :: JORDAN1H:70
for b1 being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat
for b3 being FinSequence of (TOP-REAL 2) st b3 is_sequence_on Gauge b1,b2 & len b3 > 1 holds
for b4, b5 being Nat st front_right_cell b3,((len b3) -' 1),(Gauge b1,b2) meets b1 & [b4,b5] in Indices (Gauge b1,b2) & b3 /. ((len b3) -' 1) = (Gauge b1,b2) * b4,b5 & [(b4 + 1),b5] in Indices (Gauge b1,b2) & b3 /. (len b3) = (Gauge b1,b2) * (b4 + 1),b5 holds
[(b4 + 1),(b5 -' 1)] in Indices (Gauge b1,b2)
proof end;

theorem Th71: :: JORDAN1H:71
for b1 being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat
for b3 being FinSequence of (TOP-REAL 2) st b3 is_sequence_on Gauge b1,b2 & len b3 > 1 holds
for b4, b5 being Nat st front_right_cell b3,((len b3) -' 1),(Gauge b1,b2) meets b1 & [(b5 + 1),b4] in Indices (Gauge b1,b2) & b3 /. ((len b3) -' 1) = (Gauge b1,b2) * (b5 + 1),b4 & [b5,b4] in Indices (Gauge b1,b2) & b3 /. (len b3) = (Gauge b1,b2) * b5,b4 holds
[b5,(b4 + 1)] in Indices (Gauge b1,b2)
proof end;

theorem Th72: :: JORDAN1H:72
for b1 being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat
for b3 being FinSequence of (TOP-REAL 2) st b3 is_sequence_on Gauge b1,b2 & len b3 > 1 holds
for b4, b5 being Nat st front_right_cell b3,((len b3) -' 1),(Gauge b1,b2) meets b1 & [b4,(b5 + 1)] in Indices (Gauge b1,b2) & b3 /. ((len b3) -' 1) = (Gauge b1,b2) * b4,(b5 + 1) & [b4,b5] in Indices (Gauge b1,b2) & b3 /. (len b3) = (Gauge b1,b2) * b4,b5 holds
[(b4 -' 1),b5] in Indices (Gauge b1,b2)
proof end;