for n being Nat
for A, B being Subset of (TOP-REAL n) st ( A is Bounded or B is Bounded ) holds
A /\ B is Bounded

for n being Nat
for A, B being Subset of (TOP-REAL n) st not A is Bounded & B is Bounded holds
not A \ B is Bounded

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-min (L~ (Cage C,n))) .. (Cage C,n) > 1

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-max (L~ (Cage C,n))) .. (Cage C,n) > 1

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (S-max (L~ (Cage C,n))) .. (Cage C,n) > 1

for f being non constant standard special_circular_sequence
for p being Point of (TOP-REAL 2) st p in rng f holds
left_cell f,(p .. f) = left_cell (Rotate f,p),1

for f being non constant standard special_circular_sequence
for p being Point of (TOP-REAL 2) st p in rng f holds
right_cell f,(p .. f) = right_cell (Rotate f,p),1

for n being Nat
for C being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds W-min C in right_cell (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))),1

for n being Nat
for C being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds E-max C in right_cell (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))),1

for n being Nat
for C being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds S-max C in right_cell (Rotate (Cage C,n),(S-max (L~ (Cage C,n)))),1

for f being non constant standard clockwise_oriented special_circular_sequence
for p being Point of (TOP-REAL 2) st p `1 < W-bound (L~ f) holds
p in LeftComp f

for f being non constant standard clockwise_oriented special_circular_sequence
for p being Point of (TOP-REAL 2) st p `1 > E-bound (L~ f) holds
p in LeftComp f

for f being non constant standard clockwise_oriented special_circular_sequence
for p being Point of (TOP-REAL 2) st p `2 < S-bound (L~ f) holds
p in LeftComp f

for f being non constant standard clockwise_oriented special_circular_sequence
for p being Point of (TOP-REAL 2) st p `2 > N-bound (L~ f) holds
p in LeftComp f

for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i + 1),j & f /. (k + 1) = G * i,j holds
j < width G

for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * i,j & f /. (k + 1) = G * i,(j + 1) holds
i < len G

for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * i,j & f /. (k + 1) = G * (i + 1),j holds
j > 1

for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * i,(j + 1) & f /. (k + 1) = G * i,j holds
i > 1

for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i + 1),j & f /. (k + 1) = G * i,j holds
(f /. k) `2 <> N-bound (L~ f)

for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * i,j & f /. (k + 1) = G * i,(j + 1) holds
(f /. k) `1 <> E-bound (L~ f)

for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * i,j & f /. (k + 1) = G * (i + 1),j holds
(f /. k) `2 <> S-bound (L~ f)

for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * i,(j + 1) & f /. (k + 1) = G * i,j holds
(f /. k) `1 <> W-bound (L~ f)

for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board
for k being Nat st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = W-min (L~ f) holds
ex i, j being Nat st
( [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * i,j & f /. (k + 1) = G * i,(j + 1) )

for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board
for k being Nat st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = N-min (L~ f) holds
ex i, j being Nat st
( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * i,j & f /. (k + 1) = G * (i + 1),j )

for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board
for k being Nat st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = E-max (L~ f) holds
ex i, j being Nat st
( [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * i,(j + 1) & f /. (k + 1) = G * i,j )

for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board
for k being Nat st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = S-max (L~ f) holds
ex i, j being Nat st
( [(i + 1),j] in Indices G & [i,j] in Indices G & f /. k = G * (i + 1),j & f /. (k + 1) = G * i,j )

for f being non constant standard special_circular_sequence holds
( f is clockwise_oriented iff (Rotate f,(W-min (L~ f))) /. 2 in W-most (L~ f) )

for f being non constant standard special_circular_sequence holds
( f is clockwise_oriented iff (Rotate f,(E-max (L~ f))) /. 2 in E-most (L~ f) )

for f being non constant standard special_circular_sequence holds
( f is clockwise_oriented iff (Rotate f,(S-max (L~ f))) /. 2 in S-most (L~ f) )

for i, k being Nat
for C being non empty compact non horizontal non vertical being_simple_closed_curve Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge C,i) & (Gauge C,i) * (Center (Gauge C,i)),k in Upper_Arc (L~ (Cage C,i)) & p `2 = sup (proj2 .: ((LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,i) * (Center (Gauge C,i)),k)) /\ (Lower_Arc (L~ (Cage C,i))))) holds
ex j being Nat st
( 1 <= j & j <= width (Gauge C,i) & p = (Gauge C,i) * (Center (Gauge C,i)),j )