for b₁, b₂, b₃ being Nat
for b₄ being FinSequence of the carrier of (TOP-REAL 2)
for b₅ being Go-board st b₄ is_sequence_on b₅ & LSeg (b₅ * b₁,b₂),(b₅ * b₁,b₃) meets L~ b₄ & [b₁,b₂] in Indices b₅ & [b₁,b₃] in Indices b₅ & b₂ <= b₃ holds
ex b₆ being Nat st
( b₂ <= b₆ & b₆ <= b₃ & (b₅ * b₁,b₆) `2 = inf (proj2 .: ((LSeg (b₅ * b₁,b₂),(b₅ * b₁,b₃)) /\ (L~ b₄))) )

for b₁, b₂, b₃ being Nat
for b₄ being FinSequence of the carrier of (TOP-REAL 2)
for b₅ being Go-board st b₄ is_sequence_on b₅ & LSeg (b₅ * b₁,b₂),(b₅ * b₁,b₃) meets L~ b₄ & [b₁,b₂] in Indices b₅ & [b₁,b₃] in Indices b₅ & b₂ <= b₃ holds
ex b₆ being Nat st
( b₂ <= b₆ & b₆ <= b₃ & (b₅ * b₁,b₆) `2 = sup (proj2 .: ((LSeg (b₅ * b₁,b₂),(b₅ * b₁,b₃)) /\ (L~ b₄))) )

for b₁, b₂, b₃ being Nat
for b₄ being FinSequence of the carrier of (TOP-REAL 2)
for b₅ being Go-board st b₄ is_sequence_on b₅ & LSeg (b₅ * b₁,b₂),(b₅ * b₃,b₂) meets L~ b₄ & [b₁,b₂] in Indices b₅ & [b₃,b₂] in Indices b₅ & b₁ <= b₃ holds
ex b₆ being Nat st
( b₁ <= b₆ & b₆ <= b₃ & (b₅ * b₆,b₂) `1 = inf (proj1 .: ((LSeg (b₅ * b₁,b₂),(b₅ * b₃,b₂)) /\ (L~ b₄))) )

for b₁, b₂, b₃ being Nat
for b₄ being FinSequence of the carrier of (TOP-REAL 2)
for b₅ being Go-board st b₄ is_sequence_on b₅ & LSeg (b₅ * b₁,b₂),(b₅ * b₃,b₂) meets L~ b₄ & [b₁,b₂] in Indices b₅ & [b₃,b₂] in Indices b₅ & b₁ <= b₃ holds
ex b₆ being Nat st
( b₁ <= b₆ & b₆ <= b₃ & (b₅ * b₆,b₂) `1 = sup (proj1 .: ((LSeg (b₅ * b₁,b₂),(b₅ * b₃,b₂)) /\ (L~ b₄))) )

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Nat holds (Upper_Seq b₁,b₂) /. 1 = W-min (L~ (Cage b₁,b₂))

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Nat holds (Lower_Seq b₁,b₂) /. 1 = E-max (L~ (Cage b₁,b₂))

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Nat holds (Upper_Seq b₁,b₂) /. (len (Upper_Seq b₁,b₂)) = E-max (L~ (Cage b₁,b₂))

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Nat holds (Lower_Seq b₁,b₂) /. (len (Lower_Seq b₁,b₂)) = W-min (L~ (Cage b₁,b₂))

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Nat holds
( ( L~ (Upper_Seq b₁,b₂) = Upper_Arc (L~ (Cage b₁,b₂)) & L~ (Lower_Seq b₁,b₂) = Lower_Arc (L~ (Cage b₁,b₂)) ) or ( L~ (Upper_Seq b₁,b₂) = Lower_Arc (L~ (Cage b₁,b₂)) & L~ (Lower_Seq b₁,b₂) = Upper_Arc (L~ (Cage b₁,b₂)) ) )

for b₁ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Nat holds Upper_Seq b₁,b₂ is_sequence_on Gauge b₁,b₂

for b₁ being Go-board
for b₂ being Point of (TOP-REAL 2)
for b₃ being FinSequence of (TOP-REAL 2) st b₃ is_sequence_on b₁ & ex b₄, b₅ being Nat st
( [b₄,b₅] in Indices b₁ & b₂ = b₁ * b₄,b₅ ) & ( for b₄, b₅, b₆, b₇ being Nat st [b₄,b₅] in Indices b₁ & [b₆,b₇] in Indices b₁ & b₂ = b₁ * b₄,b₅ & b₃ /. 1 = b₁ * b₆,b₇ holds
(abs (b₆ - b₄)) + (abs (b₇ - b₅)) = 1 ) holds
<*b₂*> ^ b₃ is_sequence_on b₁

for b₁ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Nat holds Lower_Seq b₁,b₂ is_sequence_on Gauge b₁,b₂

for b₁ being Nat
for b₂ being non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₃ `1 = ((W-bound b<sub>2</sub>) + (E-bound b<sub>2</sub>)) / 2 & b<sub>3</sub> `2 = inf (proj2 .: ((LSeg ((Gauge b₂,1) * (Center (Gauge b₂,1)),1),((Gauge b₂,1) * (Center (Gauge b₂,1)),(width (Gauge b₂,1)))) /\ (Upper_Arc (L~ (Cage b₂,(b₁ + 1)))))) holds
ex b₄ being Nat st
( 1 <= b₄ & b₄ <= width (Gauge b₂,(b₁ + 1)) & b₃ = (Gauge b₂,(b₁ + 1)) * (Center (Gauge b₂,(b₁ + 1))),b₄ )