environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, FINSEQ_1, EUCLID, PRE_TOPC, TOPREAL1, JORDAN3, XXREAL_0, XBOOLE_0, CARD_1, ARYTM_3, GROUP_2, PARTFUN1, FINSEQ_5, FUNCT_1, RELAT_1, FINSEQ_6, ARYTM_1, FINSEQ_4, RFINSEQ, ORDINAL4, RCOMP_1, SPPOL_1, JORDAN9, RLTOPSP1, NAT_1, TARSKI, GRAPH_2, MCART_1, REAL_1, SUPINF_2, JORDAN2C, SPPOL_2, JORDAN18, GOBOARD1, GOBOARD2, GOBOARD5, MATRIX_1, JORDAN23;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, RFINSEQ, MATRIX_0, FINSEQ_6, GRAPH_2, STRUCT_0, PRE_TOPC, NAT_D, COMPTS_1, RLVECT_1, RLTOPSP1, EUCLID, GOBOARD1, TOPREAL1, GOBOARD2, GOBOARD5, SPPOL_1, SPPOL_2, JORDAN3, JORDAN5C, JORDAN9, JORDAN2C, JORDAN18;
definitions TARSKI, XBOOLE_0, FUNCT_1;
theorems NAT_1, FINSEQ_1, FINSEQ_4, EUCLID, FINSEQ_3, SPPOL_2, TARSKI, JORDAN3, FINSEQ_5, FINSEQ_6, GOBOARD7, TOPREAL1, JORDAN5B, SPRECT_2, SPPOL_1, FINSEQ_2, JORDAN4, GOBOARD2, SPRECT_3, TOPREAL3, JORDAN8, PARTFUN2, XBOOLE_0, XBOOLE_1, ZFMISC_1, JORDAN1E, REVROT_1, JORDAN1B, JORDAN1J, GOBOARD3, TOPREAL8, GRAPH_2, JORDAN18, JORDAN5C, MSUALG_8, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1, XREAL_0, NAT_D, RLTOPSP1, RFINSEQ, SEQ_4, RLVECT_1;
schemes ;
registrations RELAT_1, FUNCT_1, XXREAL_0, XREAL_0, FINSEQ_1, FINSEQ_6, STRUCT_0, GOBOARD2, SPPOL_2, SPRECT_1, REVROT_1, TOPREAL6, JORDAN1J, ORDINAL1, CARD_1, EUCLID, SPRECT_5, ZFMISC_1, SUBSET_1;
constructors HIDDEN, REAL_1, FINSEQ_4, REALSET1, RFINSEQ, NAT_D, FINSEQ_5, GOBOARD2, GRAPH_2, JORDAN3, JORDAN5C, SPRECT_1, JORDAN2C, JORDAN9, JORDAN18, GOBOARD1, RELSET_1;
requirements HIDDEN, ARITHM, NUMERALS, BOOLE, SUBSET, REAL;
equalities XBOOLE_0, RLTOPSP1;
expansions TARSKI, XBOOLE_0, FUNCT_1;
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
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 non
constant standard special_circular_sequence st
g = B1 ^' P ) ) )