:: JORDAN1I semantic presentation

theorem Th1: :: JORDAN1I:1
for b1 being Nat
for b2, b3 being Subset of (TOP-REAL b1) st ( b2 is Bounded or b3 is Bounded ) holds
b2 /\ b3 is Bounded
proof end;

theorem Th2: :: JORDAN1I:2
for b1 being Nat
for b2, b3 being Subset of (TOP-REAL b1) st not b2 is Bounded & b3 is Bounded holds
not b2 \ b3 is Bounded
proof end;

theorem Th3: :: JORDAN1I:3
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-min (L~ (Cage b2,b1))) .. (Cage b2,b1) > 1
proof end;

theorem Th4: :: JORDAN1I:4
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-max (L~ (Cage b2,b1))) .. (Cage b2,b1) > 1
proof end;

theorem Th5: :: JORDAN1I:5
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (S-max (L~ (Cage b2,b1))) .. (Cage b2,b1) > 1
proof end;

theorem Th6: :: JORDAN1I:6
for b1 being non constant standard special_circular_sequence
for b2 being Point of (TOP-REAL 2) st b2 in rng b1 holds
left_cell b1,(b2 .. b1) = left_cell (Rotate b1,b2),1
proof end;

theorem Th7: :: JORDAN1I:7
for b1 being non constant standard special_circular_sequence
for b2 being Point of (TOP-REAL 2) st b2 in rng b1 holds
right_cell b1,(b2 .. b1) = right_cell (Rotate b1,b2),1
proof end;

theorem Th8: :: JORDAN1I:8
for b1 being Nat
for b2 being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds W-min b2 in right_cell (Rotate (Cage b2,b1),(W-min (L~ (Cage b2,b1)))),1
proof end;

theorem Th9: :: JORDAN1I:9
for b1 being Nat
for b2 being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds E-max b2 in right_cell (Rotate (Cage b2,b1),(E-max (L~ (Cage b2,b1)))),1
proof end;

theorem Th10: :: JORDAN1I:10
for b1 being Nat
for b2 being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds S-max b2 in right_cell (Rotate (Cage b2,b1),(S-max (L~ (Cage b2,b1)))),1
proof end;

theorem Th11: :: JORDAN1I:11
for b1 being non constant standard clockwise_oriented special_circular_sequence
for b2 being Point of (TOP-REAL 2) st b2 `1 < W-bound (L~ b1) holds
b2 in LeftComp b1
proof end;

theorem Th12: :: JORDAN1I:12
for b1 being non constant standard clockwise_oriented special_circular_sequence
for b2 being Point of (TOP-REAL 2) st b2 `1 > E-bound (L~ b1) holds
b2 in LeftComp b1
proof end;

theorem Th13: :: JORDAN1I:13
for b1 being non constant standard clockwise_oriented special_circular_sequence
for b2 being Point of (TOP-REAL 2) st b2 `2 < S-bound (L~ b1) holds
b2 in LeftComp b1
proof end;

theorem Th14: :: JORDAN1I:14
for b1 being non constant standard clockwise_oriented special_circular_sequence
for b2 being Point of (TOP-REAL 2) st b2 `2 > N-bound (L~ b1) holds
b2 in LeftComp b1
proof end;

theorem Th15: :: JORDAN1I:15
for b1 being non constant standard clockwise_oriented special_circular_sequence
for b2 being Go-board st b1 is_sequence_on b2 holds
for b3, b4, b5 being Nat st 1 <= b5 & b5 + 1 <= len b1 & [b3,b4] in Indices b2 & [(b3 + 1),b4] in Indices b2 & b1 /. b5 = b2 * (b3 + 1),b4 & b1 /. (b5 + 1) = b2 * b3,b4 holds
b4 < width b2
proof end;

theorem Th16: :: JORDAN1I:16
for b1 being non constant standard clockwise_oriented special_circular_sequence
for b2 being Go-board st b1 is_sequence_on b2 holds
for b3, b4, b5 being Nat st 1 <= b5 & b5 + 1 <= len b1 & [b3,b4] in Indices b2 & [b3,(b4 + 1)] in Indices b2 & b1 /. b5 = b2 * b3,b4 & b1 /. (b5 + 1) = b2 * b3,(b4 + 1) holds
b3 < len b2
proof end;

theorem Th17: :: JORDAN1I:17
for b1 being non constant standard clockwise_oriented special_circular_sequence
for b2 being Go-board st b1 is_sequence_on b2 holds
for b3, b4, b5 being Nat st 1 <= b5 & b5 + 1 <= len b1 & [b3,b4] in Indices b2 & [(b3 + 1),b4] in Indices b2 & b1 /. b5 = b2 * b3,b4 & b1 /. (b5 + 1) = b2 * (b3 + 1),b4 holds
b4 > 1
proof end;

theorem Th18: :: JORDAN1I:18
for b1 being non constant standard clockwise_oriented special_circular_sequence
for b2 being Go-board st b1 is_sequence_on b2 holds
for b3, b4, b5 being Nat st 1 <= b5 & b5 + 1 <= len b1 & [b3,b4] in Indices b2 & [b3,(b4 + 1)] in Indices b2 & b1 /. b5 = b2 * b3,(b4 + 1) & b1 /. (b5 + 1) = b2 * b3,b4 holds
b3 > 1
proof end;

theorem Th19: :: JORDAN1I:19
for b1 being non constant standard clockwise_oriented special_circular_sequence
for b2 being Go-board st b1 is_sequence_on b2 holds
for b3, b4, b5 being Nat st 1 <= b5 & b5 + 1 <= len b1 & [b3,b4] in Indices b2 & [(b3 + 1),b4] in Indices b2 & b1 /. b5 = b2 * (b3 + 1),b4 & b1 /. (b5 + 1) = b2 * b3,b4 holds
(b1 /. b5) `2 <> N-bound (L~ b1)
proof end;

theorem Th20: :: JORDAN1I:20
for b1 being non constant standard clockwise_oriented special_circular_sequence
for b2 being Go-board st b1 is_sequence_on b2 holds
for b3, b4, b5 being Nat st 1 <= b5 & b5 + 1 <= len b1 & [b3,b4] in Indices b2 & [b3,(b4 + 1)] in Indices b2 & b1 /. b5 = b2 * b3,b4 & b1 /. (b5 + 1) = b2 * b3,(b4 + 1) holds
(b1 /. b5) `1 <> E-bound (L~ b1)
proof end;

theorem Th21: :: JORDAN1I:21
for b1 being non constant standard clockwise_oriented special_circular_sequence
for b2 being Go-board st b1 is_sequence_on b2 holds
for b3, b4, b5 being Nat st 1 <= b5 & b5 + 1 <= len b1 & [b3,b4] in Indices b2 & [(b3 + 1),b4] in Indices b2 & b1 /. b5 = b2 * b3,b4 & b1 /. (b5 + 1) = b2 * (b3 + 1),b4 holds
(b1 /. b5) `2 <> S-bound (L~ b1)
proof end;

theorem Th22: :: JORDAN1I:22
for b1 being non constant standard clockwise_oriented special_circular_sequence
for b2 being Go-board st b1 is_sequence_on b2 holds
for b3, b4, b5 being Nat st 1 <= b5 & b5 + 1 <= len b1 & [b3,b4] in Indices b2 & [b3,(b4 + 1)] in Indices b2 & b1 /. b5 = b2 * b3,(b4 + 1) & b1 /. (b5 + 1) = b2 * b3,b4 holds
(b1 /. b5) `1 <> W-bound (L~ b1)
proof end;

theorem Th23: :: JORDAN1I:23
for b1 being non constant standard clockwise_oriented special_circular_sequence
for b2 being Go-board
for b3 being Nat st b1 is_sequence_on b2 & 1 <= b3 & b3 + 1 <= len b1 & b1 /. b3 = W-min (L~ b1) holds
ex b4, b5 being Nat st
( [b4,b5] in Indices b2 & [b4,(b5 + 1)] in Indices b2 & b1 /. b3 = b2 * b4,b5 & b1 /. (b3 + 1) = b2 * b4,(b5 + 1) )
proof end;

theorem Th24: :: JORDAN1I:24
for b1 being non constant standard clockwise_oriented special_circular_sequence
for b2 being Go-board
for b3 being Nat st b1 is_sequence_on b2 & 1 <= b3 & b3 + 1 <= len b1 & b1 /. b3 = N-min (L~ b1) holds
ex b4, b5 being Nat st
( [b4,b5] in Indices b2 & [(b4 + 1),b5] in Indices b2 & b1 /. b3 = b2 * b4,b5 & b1 /. (b3 + 1) = b2 * (b4 + 1),b5 )
proof end;

theorem Th25: :: JORDAN1I:25
for b1 being non constant standard clockwise_oriented special_circular_sequence
for b2 being Go-board
for b3 being Nat st b1 is_sequence_on b2 & 1 <= b3 & b3 + 1 <= len b1 & b1 /. b3 = E-max (L~ b1) holds
ex b4, b5 being Nat st
( [b4,(b5 + 1)] in Indices b2 & [b4,b5] in Indices b2 & b1 /. b3 = b2 * b4,(b5 + 1) & b1 /. (b3 + 1) = b2 * b4,b5 )
proof end;

theorem Th26: :: JORDAN1I:26
for b1 being non constant standard clockwise_oriented special_circular_sequence
for b2 being Go-board
for b3 being Nat st b1 is_sequence_on b2 & 1 <= b3 & b3 + 1 <= len b1 & b1 /. b3 = S-max (L~ b1) holds
ex b4, b5 being Nat st
( [(b4 + 1),b5] in Indices b2 & [b4,b5] in Indices b2 & b1 /. b3 = b2 * (b4 + 1),b5 & b1 /. (b3 + 1) = b2 * b4,b5 )
proof end;

theorem Th27: :: JORDAN1I:27
for b1 being non constant standard special_circular_sequence holds
( b1 is clockwise_oriented iff (Rotate b1,(W-min (L~ b1))) /. 2 in W-most (L~ b1) )
proof end;

theorem Th28: :: JORDAN1I:28
for b1 being non constant standard special_circular_sequence holds
( b1 is clockwise_oriented iff (Rotate b1,(E-max (L~ b1))) /. 2 in E-most (L~ b1) )
proof end;

theorem Th29: :: JORDAN1I:29
for b1 being non constant standard special_circular_sequence holds
( b1 is clockwise_oriented iff (Rotate b1,(S-max (L~ b1))) /. 2 in S-most (L~ b1) )
proof end;

theorem Th30: :: JORDAN1I:30
for b1, b2 being Nat
for b3 being non empty compact non horizontal non vertical being_simple_closed_curve Subset of (TOP-REAL 2)
for b4 being Point of (TOP-REAL 2) st b4 `1 = ((W-bound b3) + (E-bound b3)) / 2 & b1 > 0 & 1 <= b2 & b2 <= width (Gauge b3,b1) & (Gauge b3,b1) * (Center (Gauge b3,b1)),b2 in Upper_Arc (L~ (Cage b3,b1)) & b4 `2 = sup (proj2 .: ((LSeg ((Gauge b3,1) * (Center (Gauge b3,1)),1),((Gauge b3,b1) * (Center (Gauge b3,b1)),b2)) /\ (Lower_Arc (L~ (Cage b3,b1))))) holds
ex b5 being Nat st
( 1 <= b5 & b5 <= width (Gauge b3,b1) & b4 = (Gauge b3,b1) * (Center (Gauge b3,b1)),b5 )
proof end;