theorem
for
n being
Nat for
C being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
p,
q being
Point of
(TOP-REAL 2) st
p in BDD (L~ (Cage (C,n))) holds
ex
B being
S-Sequence_in_R2 st
(
B = B_Cut (
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),
(South-Bound (p,(L~ (Cage (C,n))))),
(North-Bound (p,(L~ (Cage (C,n)))))) & ex
P being
S-Sequence_in_R2 st
(
P is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) &
L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ P &
P /. 1
= North-Bound (
p,
(L~ (Cage (C,n)))) &
P /. (len P) = South-Bound (
p,
(L~ (Cage (C,n)))) &
len P >= 2 & ex
B1 being
S-Sequence_in_R2 st
(
B1 is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) &
L~ B = L~ B1 &
B /. 1
= B1 /. 1 &
B /. (len B) = B1 /. (len B1) &
len B <= len B1 & ex
g being
V22()
standard special_circular_sequence st
g = B1 ^' P ) ) )