begin
theorem Th1:
theorem
theorem Th3:
:: deftheorem Def1 defines almost-one-to-one JORDAN23:def 1 :
:: deftheorem Def2 defines weakly-one-to-one JORDAN23:def 2 :
:: deftheorem Def3 defines poorly-one-to-one JORDAN23:def 3 :
theorem
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem
theorem Th23:
theorem
theorem Th25:
theorem
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem
theorem Th32:
theorem Th33:
theorem
theorem Th35:
theorem Th36:
theorem
theorem Th38:
theorem Th39:
theorem Th40:
theorem
theorem Th42:
Lm1:
for f being non empty FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & q in L~ f & p <> q & p <> f . 1 & ( Index p,f < Index q,f or ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ) holds
B_Cut f,p,q is_S-Seq_joining p,q
theorem Th43:
theorem
theorem
for
n being
Element of
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 non
constant standard special_circular_sequence st
g = B1 ^' P ) ) )