:: JORDAN15 semantic presentation

theorem Th1: :: JORDAN15:1
for b1, b2 being Subset of (TOP-REAL 2) st b1 meets b2 holds
proj1 .: b1 meets proj1 .: b2
proof end;

theorem Th2: :: JORDAN15:2
for b1, b2 being Subset of (TOP-REAL 2)
for b3 being real number st b1 misses b2 & b1 c= Horizontal_Line b3 & b2 c= Horizontal_Line b3 holds
proj1 .: b1 misses proj1 .: b2
proof end;

theorem Th3: :: JORDAN15:3
for b1 being closed Subset of (TOP-REAL 2) st b1 is Bounded holds
proj1 .: b1 is closed
proof end;

theorem Th4: :: JORDAN15:4
for b1 being compact Subset of (TOP-REAL 2) holds proj1 .: b1 is compact
proof end;

theorem Th5: :: JORDAN15:5
for b1, b2, b3, b4 being Point of (TOP-REAL 2) st LSeg b1,b2 is vertical & LSeg b3,b4 is vertical & b1 `1 = b3 `1 & b1 `2 <= b3 `2 & b3 `2 <= b4 `2 & b4 `2 <= b2 `2 holds
LSeg b3,b4 c= LSeg b1,b2
proof end;

theorem Th6: :: JORDAN15:6
for b1, b2, b3, b4 being Point of (TOP-REAL 2) st LSeg b1,b2 is horizontal & LSeg b3,b4 is horizontal & b1 `2 = b3 `2 & b1 `1 <= b3 `1 & b3 `1 <= b4 `1 & b4 `1 <= b2 `1 holds
LSeg b3,b4 c= LSeg b1,b2
proof end;

theorem Th7: :: JORDAN15:7
for b1 being Go-board
for b2, b3, b4, b5, b6 being Nat st 1 <= b2 & b2 <= len b1 & 1 <= b3 & b3 <= b5 & b5 <= b6 & b6 <= b4 & b4 <= width b1 holds
LSeg (b1 * b2,b5),(b1 * b2,b6) c= LSeg (b1 * b2,b3),(b1 * b2,b4)
proof end;

theorem Th8: :: JORDAN15:8
for b1 being Go-board
for b2, b3, b4, b5, b6 being Nat st 1 <= b2 & b2 <= width b1 & 1 <= b3 & b3 <= b5 & b5 <= b6 & b6 <= b4 & b4 <= len b1 holds
LSeg (b1 * b5,b2),(b1 * b6,b2) c= LSeg (b1 * b3,b2),(b1 * b4,b2)
proof end;

theorem Th9: :: JORDAN15:9
for b1 being Go-board
for b2, b3, b4, b5 being Nat st 1 <= b2 & b2 <= b4 & b4 <= b5 & b5 <= b3 & b3 <= width b1 holds
LSeg (b1 * (Center b1),b4),(b1 * (Center b1),b5) c= LSeg (b1 * (Center b1),b2),(b1 * (Center b1),b3)
proof end;

theorem Th10: :: JORDAN15:10
for b1 being Go-board st len b1 = width b1 holds
for b2, b3, b4, b5 being Nat st 1 <= b2 & b2 <= b4 & b4 <= b5 & b5 <= b3 & b3 <= len b1 holds
LSeg (b1 * b4,(Center b1)),(b1 * b5,(Center b1)) c= LSeg (b1 * b2,(Center b1)),(b1 * b3,(Center b1))
proof end;

theorem Th11: :: JORDAN15:11
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3, b4, b5 being Nat st 1 <= b3 & b3 <= len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & (Gauge b2,b1) * b3,b4 in L~ (Lower_Seq b2,b1) holds
ex b6 being Nat st
( b4 <= b6 & b6 <= b5 & (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b3,b5)) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b3,b6)} )
proof end;

theorem Th12: :: JORDAN15:12
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3, b4, b5 being Nat st 1 <= b3 & b3 <= len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & (Gauge b2,b1) * b3,b5 in L~ (Upper_Seq b2,b1) holds
ex b6 being Nat st
( b4 <= b6 & b6 <= b5 & (LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b6)) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b3,b6)} )
proof end;

theorem Th13: :: JORDAN15:13
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3, b4, b5 being Nat st 1 <= b3 & b3 <= len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & (Gauge b2,b1) * b3,b4 in L~ (Lower_Seq b2,b1) & (Gauge b2,b1) * b3,b5 in L~ (Upper_Seq b2,b1) holds
ex b6, b7 being Nat st
( b4 <= b6 & b6 <= b7 & b7 <= b5 & (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b3,b7)) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b3,b6)} & (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b3,b7)) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b3,b7)} )
proof end;

theorem Th14: :: JORDAN15:14
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3, b4, b5 being Nat st 1 <= b4 & b4 <= b5 & b5 <= len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & (Gauge b2,b1) * b4,b3 in L~ (Lower_Seq b2,b1) holds
ex b6 being Nat st
( b4 <= b6 & b6 <= b5 & (LSeg ((Gauge b2,b1) * b6,b3),((Gauge b2,b1) * b5,b3)) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b6,b3)} )
proof end;

theorem Th15: :: JORDAN15:15
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3, b4, b5 being Nat st 1 <= b4 & b4 <= b5 & b5 <= len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & (Gauge b2,b1) * b5,b3 in L~ (Upper_Seq b2,b1) holds
ex b6 being Nat st
( b4 <= b6 & b6 <= b5 & (LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b6,b3)) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b6,b3)} )
proof end;

theorem Th16: :: JORDAN15:16
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3, b4, b5 being Nat st 1 <= b4 & b4 <= b5 & b5 <= len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & (Gauge b2,b1) * b4,b3 in L~ (Lower_Seq b2,b1) & (Gauge b2,b1) * b5,b3 in L~ (Upper_Seq b2,b1) holds
ex b6, b7 being Nat st
( b4 <= b6 & b6 <= b7 & b7 <= b5 & (LSeg ((Gauge b2,b1) * b6,b3),((Gauge b2,b1) * b7,b3)) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b6,b3)} & (LSeg ((Gauge b2,b1) * b6,b3),((Gauge b2,b1) * b7,b3)) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b7,b3)} )
proof end;

theorem Th17: :: JORDAN15:17
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3, b4, b5 being Nat st 1 <= b3 & b3 <= len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & (Gauge b2,b1) * b3,b4 in L~ (Upper_Seq b2,b1) holds
ex b6 being Nat st
( b4 <= b6 & b6 <= b5 & (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b3,b5)) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b3,b6)} )
proof end;

theorem Th18: :: JORDAN15:18
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3, b4, b5 being Nat st 1 <= b3 & b3 <= len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & (Gauge b2,b1) * b3,b5 in L~ (Lower_Seq b2,b1) holds
ex b6 being Nat st
( b4 <= b6 & b6 <= b5 & (LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b6)) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b3,b6)} )
proof end;

theorem Th19: :: JORDAN15:19
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3, b4, b5 being Nat st 1 <= b3 & b3 <= len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & (Gauge b2,b1) * b3,b4 in L~ (Upper_Seq b2,b1) & (Gauge b2,b1) * b3,b5 in L~ (Lower_Seq b2,b1) holds
ex b6, b7 being Nat st
( b4 <= b6 & b6 <= b7 & b7 <= b5 & (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b3,b7)) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b3,b6)} & (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b3,b7)) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b3,b7)} )
proof end;

theorem Th20: :: JORDAN15:20
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3, b4, b5 being Nat st 1 <= b4 & b4 <= b5 & b5 <= len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & (Gauge b2,b1) * b4,b3 in L~ (Upper_Seq b2,b1) holds
ex b6 being Nat st
( b4 <= b6 & b6 <= b5 & (LSeg ((Gauge b2,b1) * b6,b3),((Gauge b2,b1) * b5,b3)) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b6,b3)} )
proof end;

theorem Th21: :: JORDAN15:21
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3, b4, b5 being Nat st 1 <= b4 & b4 <= b5 & b5 <= len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & (Gauge b2,b1) * b5,b3 in L~ (Lower_Seq b2,b1) holds
ex b6 being Nat st
( b4 <= b6 & b6 <= b5 & (LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b6,b3)) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b6,b3)} )
proof end;

theorem Th22: :: JORDAN15:22
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3, b4, b5 being Nat st 1 <= b4 & b4 <= b5 & b5 <= len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & (Gauge b2,b1) * b4,b3 in L~ (Upper_Seq b2,b1) & (Gauge b2,b1) * b5,b3 in L~ (Lower_Seq b2,b1) holds
ex b6, b7 being Nat st
( b4 <= b6 & b6 <= b7 & b7 <= b5 & (LSeg ((Gauge b2,b1) * b6,b3),((Gauge b2,b1) * b7,b3)) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b6,b3)} & (LSeg ((Gauge b2,b1) * b6,b3),((Gauge b2,b1) * b7,b3)) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b7,b3)} )
proof end;

theorem Th23: :: JORDAN15:23
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & (Gauge b2,b1) * b3,b5 in L~ (Upper_Seq b2,b1) & (Gauge b2,b1) * b3,b4 in L~ (Lower_Seq b2,b1) holds
LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5) meets Lower_Arc b2
proof end;

theorem Th24: :: JORDAN15:24
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & (Gauge b2,b1) * b3,b5 in L~ (Upper_Seq b2,b1) & (Gauge b2,b1) * b3,b4 in L~ (Lower_Seq b2,b1) holds
LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5) meets Upper_Arc b2
proof end;

theorem Th25: :: JORDAN15:25
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & b1 > 0 & (Gauge b2,b1) * b3,b5 in Upper_Arc (L~ (Cage b2,b1)) & (Gauge b2,b1) * b3,b4 in Lower_Arc (L~ (Cage b2,b1)) holds
LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5) meets Lower_Arc b2
proof end;

theorem Th26: :: JORDAN15:26
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & b1 > 0 & (Gauge b2,b1) * b3,b5 in Upper_Arc (L~ (Cage b2,b1)) & (Gauge b2,b1) * b3,b4 in Lower_Arc (L~ (Cage b2,b1)) holds
LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5) meets Upper_Arc b2
proof end;

theorem Th27: :: JORDAN15:27
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4 being Nat st 1 <= b3 & b3 <= b4 & b4 <= width (Gauge b2,(b1 + 1)) & (Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b4 in Upper_Arc (L~ (Cage b2,(b1 + 1))) & (Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b3 in Lower_Arc (L~ (Cage b2,(b1 + 1))) holds
LSeg ((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b3),((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b4) meets Lower_Arc b2
proof end;

theorem Th28: :: JORDAN15:28
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4 being Nat st 1 <= b3 & b3 <= b4 & b4 <= width (Gauge b2,(b1 + 1)) & (Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b4 in Upper_Arc (L~ (Cage b2,(b1 + 1))) & (Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b3 in Lower_Arc (L~ (Cage b2,(b1 + 1))) holds
LSeg ((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b3),((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b4) meets Upper_Arc b2
proof end;

theorem Th29: :: JORDAN15:29
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3, b4, b5 being Nat st 1 < b4 & b5 < len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & (Gauge b2,b1) * b5,b3 in L~ (Upper_Seq b2,b1) & (Gauge b2,b1) * b4,b3 in L~ (Lower_Seq b2,b1) holds
b4 <> b5
proof end;

theorem Th30: :: JORDAN15:30
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b4 & b4 <= b5 & b5 < len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & (LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3)) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b5,b3)} & (LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3)) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b4,b3)} holds
LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3) meets Lower_Arc b2
proof end;

theorem Th31: :: JORDAN15:31
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b4 & b4 <= b5 & b5 < len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & (LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3)) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b5,b3)} & (LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3)) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b4,b3)} holds
LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3) meets Upper_Arc b2
proof end;

theorem Th32: :: JORDAN15:32
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b4 & b4 <= b5 & b5 < len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & (Gauge b2,b1) * b5,b3 in L~ (Upper_Seq b2,b1) & (Gauge b2,b1) * b4,b3 in L~ (Lower_Seq b2,b1) holds
LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3) meets Lower_Arc b2
proof end;

theorem Th33: :: JORDAN15:33
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b4 & b4 <= b5 & b5 < len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & (Gauge b2,b1) * b5,b3 in L~ (Upper_Seq b2,b1) & (Gauge b2,b1) * b4,b3 in L~ (Lower_Seq b2,b1) holds
LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3) meets Upper_Arc b2
proof end;

theorem Th34: :: JORDAN15:34
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b4 & b4 <= b5 & b5 < len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & b1 > 0 & (Gauge b2,b1) * b5,b3 in Upper_Arc (L~ (Cage b2,b1)) & (Gauge b2,b1) * b4,b3 in Lower_Arc (L~ (Cage b2,b1)) holds
LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3) meets Lower_Arc b2
proof end;

theorem Th35: :: JORDAN15:35
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b4 & b4 <= b5 & b5 < len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & b1 > 0 & (Gauge b2,b1) * b5,b3 in Upper_Arc (L~ (Cage b2,b1)) & (Gauge b2,b1) * b4,b3 in Lower_Arc (L~ (Cage b2,b1)) holds
LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3) meets Upper_Arc b2
proof end;

theorem Th36: :: JORDAN15:36
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4 being Nat st 1 < b3 & b3 <= b4 & b4 < len (Gauge b2,(b1 + 1)) & (Gauge b2,(b1 + 1)) * b4,(Center (Gauge b2,(b1 + 1))) in Upper_Arc (L~ (Cage b2,(b1 + 1))) & (Gauge b2,(b1 + 1)) * b3,(Center (Gauge b2,(b1 + 1))) in Lower_Arc (L~ (Cage b2,(b1 + 1))) holds
LSeg ((Gauge b2,(b1 + 1)) * b3,(Center (Gauge b2,(b1 + 1)))),((Gauge b2,(b1 + 1)) * b4,(Center (Gauge b2,(b1 + 1)))) meets Lower_Arc b2
proof end;

theorem Th37: :: JORDAN15:37
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4 being Nat st 1 < b3 & b3 <= b4 & b4 < len (Gauge b2,(b1 + 1)) & (Gauge b2,(b1 + 1)) * b4,(Center (Gauge b2,(b1 + 1))) in Upper_Arc (L~ (Cage b2,(b1 + 1))) & (Gauge b2,(b1 + 1)) * b3,(Center (Gauge b2,(b1 + 1))) in Lower_Arc (L~ (Cage b2,(b1 + 1))) holds
LSeg ((Gauge b2,(b1 + 1)) * b3,(Center (Gauge b2,(b1 + 1)))),((Gauge b2,(b1 + 1)) * b4,(Center (Gauge b2,(b1 + 1)))) meets Upper_Arc b2
proof end;

theorem Th38: :: JORDAN15:38
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b4 & b4 <= b5 & b5 < len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & (LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3)) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b4,b3)} & (LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3)) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b5,b3)} holds
LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3) meets Lower_Arc b2
proof end;

theorem Th39: :: JORDAN15:39
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b4 & b4 <= b5 & b5 < len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & (LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3)) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b4,b3)} & (LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3)) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b5,b3)} holds
LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3) meets Upper_Arc b2
proof end;

theorem Th40: :: JORDAN15:40
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b4 & b4 <= b5 & b5 < len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & (Gauge b2,b1) * b4,b3 in L~ (Upper_Seq b2,b1) & (Gauge b2,b1) * b5,b3 in L~ (Lower_Seq b2,b1) holds
LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3) meets Lower_Arc b2
proof end;

theorem Th41: :: JORDAN15:41
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b4 & b4 <= b5 & b5 < len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & (Gauge b2,b1) * b4,b3 in L~ (Upper_Seq b2,b1) & (Gauge b2,b1) * b5,b3 in L~ (Lower_Seq b2,b1) holds
LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3) meets Upper_Arc b2
proof end;

theorem Th42: :: JORDAN15:42
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b4 & b4 <= b5 & b5 < len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & b1 > 0 & (Gauge b2,b1) * b4,b3 in Upper_Arc (L~ (Cage b2,b1)) & (Gauge b2,b1) * b5,b3 in Lower_Arc (L~ (Cage b2,b1)) holds
LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3) meets Lower_Arc b2
proof end;

theorem Th43: :: JORDAN15:43
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b4 & b4 <= b5 & b5 < len (Gauge b2,b1) & 1 <= b3 & b3 <= width (Gauge b2,b1) & b1 > 0 & (Gauge b2,b1) * b4,b3 in Upper_Arc (L~ (Cage b2,b1)) & (Gauge b2,b1) * b5,b3 in Lower_Arc (L~ (Cage b2,b1)) holds
LSeg ((Gauge b2,b1) * b4,b3),((Gauge b2,b1) * b5,b3) meets Upper_Arc b2
proof end;

theorem Th44: :: JORDAN15:44
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4 being Nat st 1 < b3 & b3 <= b4 & b4 < len (Gauge b2,(b1 + 1)) & (Gauge b2,(b1 + 1)) * b3,(Center (Gauge b2,(b1 + 1))) in Upper_Arc (L~ (Cage b2,(b1 + 1))) & (Gauge b2,(b1 + 1)) * b4,(Center (Gauge b2,(b1 + 1))) in Lower_Arc (L~ (Cage b2,(b1 + 1))) holds
LSeg ((Gauge b2,(b1 + 1)) * b3,(Center (Gauge b2,(b1 + 1)))),((Gauge b2,(b1 + 1)) * b4,(Center (Gauge b2,(b1 + 1)))) meets Lower_Arc b2
proof end;

theorem Th45: :: JORDAN15:45
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4 being Nat st 1 < b3 & b3 <= b4 & b4 < len (Gauge b2,(b1 + 1)) & (Gauge b2,(b1 + 1)) * b3,(Center (Gauge b2,(b1 + 1))) in Upper_Arc (L~ (Cage b2,(b1 + 1))) & (Gauge b2,(b1 + 1)) * b4,(Center (Gauge b2,(b1 + 1))) in Lower_Arc (L~ (Cage b2,(b1 + 1))) holds
LSeg ((Gauge b2,(b1 + 1)) * b3,(Center (Gauge b2,(b1 + 1)))),((Gauge b2,(b1 + 1)) * b4,(Center (Gauge b2,(b1 + 1)))) meets Upper_Arc b2
proof end;

theorem Th46: :: JORDAN15:46
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5, b6 being Nat st 1 < b3 & b3 <= b4 & b4 < len (Gauge b2,b1) & 1 <= b5 & b5 <= b6 & b6 <= width (Gauge b2,b1) & ((LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6))) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b4,b6)} & ((LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6))) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b3,b5)} holds
(LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6)) meets Upper_Arc b2
proof end;

theorem Th47: :: JORDAN15:47
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5, b6 being Nat st 1 < b3 & b3 <= b4 & b4 < len (Gauge b2,b1) & 1 <= b5 & b5 <= b6 & b6 <= width (Gauge b2,b1) & ((LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6))) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b4,b6)} & ((LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6))) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b3,b5)} holds
(LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6)) meets Lower_Arc b2
proof end;

theorem Th48: :: JORDAN15:48
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5, b6 being Nat st 1 < b4 & b4 <= b3 & b3 < len (Gauge b2,b1) & 1 <= b5 & b5 <= b6 & b6 <= width (Gauge b2,b1) & ((LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6))) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b4,b6)} & ((LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6))) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b3,b5)} holds
(LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6)) meets Upper_Arc b2
proof end;

theorem Th49: :: JORDAN15:49
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5, b6 being Nat st 1 < b4 & b4 <= b3 & b3 < len (Gauge b2,b1) & 1 <= b5 & b5 <= b6 & b6 <= width (Gauge b2,b1) & ((LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6))) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b4,b6)} & ((LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6))) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b3,b5)} holds
(LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6)) meets Lower_Arc b2
proof end;

theorem Th50: :: JORDAN15:50
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5, b6 being Nat st 1 < b3 & b3 < len (Gauge b2,(b1 + 1)) & 1 < b4 & b4 < len (Gauge b2,(b1 + 1)) & 1 <= b5 & b5 <= b6 & b6 <= width (Gauge b2,(b1 + 1)) & (Gauge b2,(b1 + 1)) * b3,b6 in Upper_Arc (L~ (Cage b2,(b1 + 1))) & (Gauge b2,(b1 + 1)) * b4,b5 in Lower_Arc (L~ (Cage b2,(b1 + 1))) holds
(LSeg ((Gauge b2,(b1 + 1)) * b4,b5),((Gauge b2,(b1 + 1)) * b4,b6)) \/ (LSeg ((Gauge b2,(b1 + 1)) * b4,b6),((Gauge b2,(b1 + 1)) * b3,b6)) meets Upper_Arc b2
proof end;

theorem Th51: :: JORDAN15:51
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5, b6 being Nat st 1 < b3 & b3 < len (Gauge b2,(b1 + 1)) & 1 < b4 & b4 < len (Gauge b2,(b1 + 1)) & 1 <= b5 & b5 <= b6 & b6 <= width (Gauge b2,(b1 + 1)) & (Gauge b2,(b1 + 1)) * b3,b6 in Upper_Arc (L~ (Cage b2,(b1 + 1))) & (Gauge b2,(b1 + 1)) * b4,b5 in Lower_Arc (L~ (Cage b2,(b1 + 1))) holds
(LSeg ((Gauge b2,(b1 + 1)) * b4,b5),((Gauge b2,(b1 + 1)) * b4,b6)) \/ (LSeg ((Gauge b2,(b1 + 1)) * b4,b6),((Gauge b2,(b1 + 1)) * b3,b6)) meets Lower_Arc b2
proof end;

theorem Th52: :: JORDAN15:52
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,(b1 + 1)) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,(b1 + 1)) & (Gauge b2,(b1 + 1)) * b3,b5 in Upper_Arc (L~ (Cage b2,(b1 + 1))) & (Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b4 in Lower_Arc (L~ (Cage b2,(b1 + 1))) holds
(LSeg ((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b4),((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b5)) \/ (LSeg ((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b5),((Gauge b2,(b1 + 1)) * b3,b5)) meets Upper_Arc b2
proof end;

theorem Th53: :: JORDAN15:53
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,(b1 + 1)) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,(b1 + 1)) & (Gauge b2,(b1 + 1)) * b3,b5 in Upper_Arc (L~ (Cage b2,(b1 + 1))) & (Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b4 in Lower_Arc (L~ (Cage b2,(b1 + 1))) holds
(LSeg ((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b4),((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b5)) \/ (LSeg ((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b5),((Gauge b2,(b1 + 1)) * b3,b5)) meets Lower_Arc b2
proof end;