:: JORDAN1E semantic presentation

REAL is V167() V168() V169() V173() set
NAT is V8() V24() cardinal limit_cardinal V167() V168() V169() V170() V171() V172() V173() Element of K27(REAL)
K27(REAL) is set
NAT is V8() V24() cardinal limit_cardinal V167() V168() V169() V170() V171() V172() V173() set
K27(NAT) is V24() set
K27(NAT) is V24() set
COMPLEX is V167() V173() set
2 is V8() V12() non empty V24() cardinal V35() V36() V37() ext-real positive non negative V156() V167() V168() V169() V170() V171() V172() Element of NAT
K28(2,2) is set
K28(K28(2,2),2) is set
K27(K28(K28(2,2),2)) is set
1 is V8() V12() non empty V24() cardinal V35() V36() V37() ext-real positive non negative V156() V167() V168() V169() V170() V171() V172() Element of NAT
K28(1,1) is set
K27(K28(1,1)) is set
K28(K28(1,1),1) is set
K27(K28(K28(1,1),1)) is set
K28(K28(1,1),REAL) is set
K27(K28(K28(1,1),REAL)) is set
K28(REAL,REAL) is set
K28(K28(REAL,REAL),REAL) is set
K27(K28(K28(REAL,REAL),REAL)) is set
K28(K28(2,2),REAL) is set
K27(K28(K28(2,2),REAL)) is set
RAT is V167() V168() V169() V170() V173() set
INT is V167() V168() V169() V170() V171() V173() set
K27(K28(REAL,REAL)) is set
TOP-REAL 2 is non empty V49() TopSpace-like V85() V110() V111() V112() V113() V114() V115() V116() strict RLTopStruct
the U1 of (TOP-REAL 2) is non empty V19() set
K28( the U1 of (TOP-REAL 2),REAL) is set
K27(K28( the U1 of (TOP-REAL 2),REAL)) is set
K27( the U1 of (TOP-REAL 2)) is set
K375( the U1 of (TOP-REAL 2)) is functional non empty FinSequence-membered M14( the U1 of (TOP-REAL 2))
{} is V8() Function-like functional empty cardinal {} -element FinSequence-membered V167() V168() V169() V170() V171() V172() V173() set
the V8() Function-like functional empty cardinal {} -element FinSequence-membered V167() V168() V169() V170() V171() V172() V173() set is V8() Function-like functional empty cardinal {} -element FinSequence-membered V167() V168() V169() V170() V171() V172() V173() set
3 is V8() V12() non empty V24() cardinal V35() V36() V37() ext-real positive non negative V156() V167() V168() V169() V170() V171() V172() Element of NAT
0 is V8() V12() Function-like functional empty V24() cardinal {} -element FinSequence-membered V35() V36() V37() ext-real non positive non negative V156() V167() V168() V169() V170() V171() V172() V173() Element of NAT
4 is V8() V12() non empty V24() cardinal V35() V36() V37() ext-real positive non negative V156() V167() V168() V169() V170() V171() V172() Element of NAT
C is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
rng n is set
k is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
n -: k is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
k .. n is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
len n is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
k9 is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
dom (n -: k) is V167() V168() V169() V170() V171() V172() Element of K27(NAT)
L~ C is Element of K27( the U1 of (TOP-REAL 2))
len C is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
{ (LSeg (C,b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len C ) } is set
union { (LSeg (C,b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len C ) } is set
W-bound (L~ C) is V35() V36() ext-real Element of REAL
(TOP-REAL 2) | (L~ C) is strict SubSpace of TOP-REAL 2
proj1 is V1() V4( the U1 of (TOP-REAL 2)) V5( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of K27(K28( the U1 of (TOP-REAL 2),REAL))
proj1 | (L~ C) is V1() V4( the U1 of ((TOP-REAL 2) | (L~ C))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (L~ C)),REAL))
the U1 of ((TOP-REAL 2) | (L~ C)) is set
K28( the U1 of ((TOP-REAL 2) | (L~ C)),REAL) is set
K27(K28( the U1 of ((TOP-REAL 2) | (L~ C)),REAL)) is set
K406(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V35() V36() ext-real Element of REAL
(n -: k) /. k9 is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
((n -: k) /. k9) `1 is V35() V36() ext-real Element of REAL
E-bound (L~ C) is V35() V36() ext-real Element of REAL
K407(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V35() V36() ext-real Element of REAL
S-bound (L~ C) is V35() V36() ext-real Element of REAL
proj2 is V1() V4( the U1 of (TOP-REAL 2)) V5( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of K27(K28( the U1 of (TOP-REAL 2),REAL))
proj2 | (L~ C) is V1() V4( the U1 of ((TOP-REAL 2) | (L~ C))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (L~ C)),REAL))
K406(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V35() V36() ext-real Element of REAL
((n -: k) /. k9) `2 is V35() V36() ext-real Element of REAL
N-bound (L~ C) is V35() V36() ext-real Element of REAL
K407(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V35() V36() ext-real Element of REAL
len (n -: k) is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
Seg (k .. n) is V24() k .. n -element V167() V168() V169() V170() V171() V172() Element of K27(NAT)
n /. k9 is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
Seg (len (n -: k)) is V24() len (n -: k) -element V167() V168() V169() V170() V171() V172() Element of K27(NAT)
dom n is V167() V168() V169() V170() V171() V172() Element of K27(NAT)
C is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
rng n is set
k is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
n :- k is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
k9 is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
dom (n :- k) is V167() V168() V169() V170() V171() V172() Element of K27(NAT)
L~ C is Element of K27( the U1 of (TOP-REAL 2))
len C is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
{ (LSeg (C,b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len C ) } is set
union { (LSeg (C,b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len C ) } is set
W-bound (L~ C) is V35() V36() ext-real Element of REAL
(TOP-REAL 2) | (L~ C) is strict SubSpace of TOP-REAL 2
proj1 is V1() V4( the U1 of (TOP-REAL 2)) V5( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of K27(K28( the U1 of (TOP-REAL 2),REAL))
proj1 | (L~ C) is V1() V4( the U1 of ((TOP-REAL 2) | (L~ C))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (L~ C)),REAL))
the U1 of ((TOP-REAL 2) | (L~ C)) is set
K28( the U1 of ((TOP-REAL 2) | (L~ C)),REAL) is set
K27(K28( the U1 of ((TOP-REAL 2) | (L~ C)),REAL)) is set
K406(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V35() V36() ext-real Element of REAL
(n :- k) /. k9 is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
((n :- k) /. k9) `1 is V35() V36() ext-real Element of REAL
E-bound (L~ C) is V35() V36() ext-real Element of REAL
K407(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V35() V36() ext-real Element of REAL
S-bound (L~ C) is V35() V36() ext-real Element of REAL
proj2 is V1() V4( the U1 of (TOP-REAL 2)) V5( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of K27(K28( the U1 of (TOP-REAL 2),REAL))
proj2 | (L~ C) is V1() V4( the U1 of ((TOP-REAL 2) | (L~ C))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (L~ C)),REAL))
K406(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V35() V36() ext-real Element of REAL
((n :- k) /. k9) `2 is V35() V36() ext-real Element of REAL
N-bound (L~ C) is V35() V36() ext-real Element of REAL
K407(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V35() V36() ext-real Element of REAL
k .. n is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
0 + 1 is V8() V12() non empty V24() cardinal V35() V36() V37() ext-real positive non negative V156() V167() V168() V169() V170() V171() V172() Element of NAT
k9 -' 1 is V8() V12() V24() cardinal V35() V36() V37() ext-real non negative V156() V167() V168() V169() V170() V171() V172() Element of NAT
(k9 -' 1) + (k .. n) is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
len (n :- k) is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len (n :- k)) is V24() len (n :- k) -element V167() V168() V169() V170() V171() V172() Element of K27(NAT)
(k9 -' 1) + 1 is V8() V12() non empty V24() cardinal V35() V36() V37() ext-real positive non negative V156() V167() V168() V169() V170() V171() V172() Element of NAT
n /. ((k9 -' 1) + (k .. n)) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
len n is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
(len n) - (k .. n) is V35() V36() ext-real set
((len n) - (k .. n)) + 1 is V35() V36() ext-real set
k9 - 1 is V35() V36() ext-real set
(k9 - 1) + (k .. n) is V35() V36() ext-real set
dom n is V167() V168() V169() V170() V171() V172() Element of K27(NAT)
n is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is Element of K27( the U1 of (TOP-REAL 2))
len n is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
{ (LSeg (n,b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len n ) } is set
union { (LSeg (n,b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len n ) } is set
C is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
L_Cut (n,C) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
dom n is V167() V168() V169() V170() V171() V172() Element of K27(NAT)
Index (C,n) is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
(Index (C,n)) + 1 is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
n . ((Index (C,n)) + 1) is set
<*C*> is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like constant non empty V19() V24() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the U1 of (TOP-REAL 2)
mid (n,((Index (C,n)) + 1),(len n)) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*C*> ^ (mid (n,((Index (C,n)) + 1),(len n))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is Element of K27( the U1 of (TOP-REAL 2))
len n is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
{ (LSeg (n,b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len n ) } is set
union { (LSeg (n,b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len n ) } is set
n . 1 is set
C is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
R_Cut (n,C) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (R_Cut (n,C)) is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
L~ (R_Cut (n,C)) is Element of K27( the U1 of (TOP-REAL 2))
{ (LSeg ((R_Cut (n,C)),b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (R_Cut (n,C)) ) } is set
union { (LSeg ((R_Cut (n,C)),b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (R_Cut (n,C)) ) } is set
0 + 1 is V8() V12() non empty V24() cardinal V35() V36() V37() ext-real positive non negative V156() V167() V168() V169() V170() V171() V172() Element of NAT
(R_Cut (n,C)) . 1 is set
n is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is Element of K27( the U1 of (TOP-REAL 2))
len n is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
{ (LSeg (n,b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len n ) } is set
union { (LSeg (n,b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len n ) } is set
n . 1 is set
C is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
Index (C,n) is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
(Index (C,n)) + 1 is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
mid (n,((Index (C,n)) + 1),(len n)) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (mid (n,((Index (C,n)) + 1),(len n))) is Element of K27( the U1 of (TOP-REAL 2))
len (mid (n,((Index (C,n)) + 1),(len n))) is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
{ (LSeg ((mid (n,((Index (C,n)) + 1),(len n))),b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (mid (n,((Index (C,n)) + 1),(len n))) ) } is set
union { (LSeg ((mid (n,((Index (C,n)) + 1),(len n))),b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (mid (n,((Index (C,n)) + 1),(len n))) ) } is set
dom n is V167() V168() V169() V170() V171() V172() Element of K27(NAT)
n /. 1 is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
0 + 1 is V8() V12() non empty V24() cardinal V35() V36() V37() ext-real positive non negative V156() V167() V168() V169() V170() V171() V172() Element of NAT
n is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
C is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
n + C is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
k is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
k9 is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
k + k9 is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
i1 is V8() V12() V24() cardinal V35() V36() ext-real set
n + i1 is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
j1 is V8() V12() V24() cardinal V35() V36() ext-real set
C + j1 is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
j1 + i1 is V35() V36() ext-real set
C + (j1 + i1) is V35() V36() ext-real set
C + 0 is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
n is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is Element of K27( the U1 of (TOP-REAL 2))
len n is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
{ (LSeg (n,b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len n ) } is set
union { (LSeg (n,b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len n ) } is set
n . 1 is set
dom n is V167() V168() V169() V170() V171() V172() Element of K27(NAT)
n /. 1 is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
C is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
L_Cut (n,C) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (L_Cut (n,C)) is Element of K27( the U1 of (TOP-REAL 2))
len (L_Cut (n,C)) is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
{ (LSeg ((L_Cut (n,C)),b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (L_Cut (n,C)) ) } is set
union { (LSeg ((L_Cut (n,C)),b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (L_Cut (n,C)) ) } is set
Index (C,n) is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
(Index (C,n)) + 1 is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
mid (n,((Index (C,n)) + 1),(len n)) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (mid (n,((Index (C,n)) + 1),(len n))) is Element of K27( the U1 of (TOP-REAL 2))
len (mid (n,((Index (C,n)) + 1),(len n))) is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
{ (LSeg ((mid (n,((Index (C,n)) + 1),(len n))),b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (mid (n,((Index (C,n)) + 1),(len n))) ) } is set
union { (LSeg ((mid (n,((Index (C,n)) + 1),(len n))),b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (mid (n,((Index (C,n)) + 1),(len n))) ) } is set
n . ((Index (C,n)) + 1) is set
<*C*> is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like constant non empty V19() V24() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the U1 of (TOP-REAL 2)
<*C*> ^ (mid (n,((Index (C,n)) + 1),(len n))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
(mid (n,((Index (C,n)) + 1),(len n))) /. 1 is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
LSeg (C,((mid (n,((Index (C,n)) + 1),(len n))) /. 1)) is connected compact compact Element of K27( the U1 of (TOP-REAL 2))
(LSeg (C,((mid (n,((Index (C,n)) + 1),(len n))) /. 1))) \/ (L~ (mid (n,((Index (C,n)) + 1),(len n)))) is Element of K27( the U1 of (TOP-REAL 2))
1 + 1 is V8() V12() non empty V24() cardinal V35() V36() V37() ext-real positive non negative V156() V167() V168() V169() V170() V171() V172() Element of NAT
len (<*C*> ^ (mid (n,((Index (C,n)) + 1),(len n)))) is V8() V12() non empty V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
k9 is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
k9 + 1 is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
LSeg ((<*C*> ^ (mid (n,((Index (C,n)) + 1),(len n)))),k9) is Element of K27( the U1 of (TOP-REAL 2))
(Index (C,n)) + k9 is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
((Index (C,n)) + k9) -' 1 is V8() V12() V24() cardinal V35() V36() V37() ext-real non negative V156() V167() V168() V169() V170() V171() V172() Element of NAT
LSeg (n,(((Index (C,n)) + k9) -' 1)) is Element of K27( the U1 of (TOP-REAL 2))
LSeg (n,1) is Element of K27( the U1 of (TOP-REAL 2))
n /. (1 + 1) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
LSeg ((n /. 1),(n /. (1 + 1))) is connected compact compact Element of K27( the U1 of (TOP-REAL 2))
n is non empty compact non horizontal non vertical Element of K27( the U1 of (TOP-REAL 2))
C is V8() V12() V24() cardinal V35() V36() ext-real set
Cage (n,C) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() V24() FinSequence-like FinSubsequence-like circular special unfolded V220() V221() clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Cage (n,C)) is non empty connected being_simple_closed_curve compact Element of K27( the U1 of (TOP-REAL 2))
len (Cage (n,C)) is V8() V12() non empty V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
{ (LSeg ((Cage (n,C)),b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Cage (n,C)) ) } is set
union { (LSeg ((Cage (n,C)),b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Cage (n,C)) ) } is set
W-min (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
W-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (n,C))) is strict SubSpace of TOP-REAL 2
proj1 is V1() V4( the U1 of (TOP-REAL 2)) V5( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of K27(K28( the U1 of (TOP-REAL 2),REAL))
proj1 | (L~ (Cage (n,C))) is V1() V4( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL))
the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))) is set
K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL) is set
K27(K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL)) is set
K406(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj1 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
W-most (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
SW-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
S-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
proj2 is V1() V4( the U1 of (TOP-REAL 2)) V5( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of K27(K28( the U1 of (TOP-REAL 2),REAL))
proj2 | (L~ (Cage (n,C))) is V1() V4( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL))
K406(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj2 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),(S-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
NW-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
N-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
K407(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj2 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),(N-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (n,C)))),(NW-corner (L~ (Cage (n,C))))) is connected compact compact Element of K27( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ (Cage (n,C)))),(NW-corner (L~ (Cage (n,C)))))) /\ (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ (Cage (n,C)))) is strict SubSpace of TOP-REAL 2
proj2 | (W-most (L~ (Cage (n,C)))) is V1() V4( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C)))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL))
the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))) is set
K28( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL) is set
K27(K28( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL)) is set
K406(((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),(proj2 | (W-most (L~ (Cage (n,C)))))) is V35() V36() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),K406(((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),(proj2 | (W-most (L~ (Cage (n,C))))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C))))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() V24() FinSequence-like FinSubsequence-like circular special unfolded V220() V221() clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
E-max (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
E-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
K407(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj1 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
E-most (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
SE-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ (Cage (n,C)))),(S-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
NE-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ (Cage (n,C)))),(N-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (n,C)))),(NE-corner (L~ (Cage (n,C))))) is connected compact compact Element of K27( the U1 of (TOP-REAL 2))
(LSeg ((SE-corner (L~ (Cage (n,C)))),(NE-corner (L~ (Cage (n,C)))))) /\ (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ (Cage (n,C)))) is strict SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (n,C)))) is V1() V4( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C)))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL))
the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))) is set
K28( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL) is set
K27(K28( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL)) is set
K407(((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),(proj2 | (E-most (L~ (Cage (n,C)))))) is V35() V36() ext-real Element of REAL
|[(E-bound (L~ (Cage (n,C)))),K407(((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),(proj2 | (E-most (L~ (Cage (n,C))))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
(Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C)))))) -: (E-max (L~ (Cage (n,C)))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like special unfolded FinSequence of the U1 of (TOP-REAL 2)
n is non empty compact non horizontal non vertical Element of K27( the U1 of (TOP-REAL 2))
C is V8() V12() V24() cardinal V35() V36() ext-real set
(n,C) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Cage (n,C) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() V24() FinSequence-like FinSubsequence-like circular special unfolded V220() V221() clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Cage (n,C)) is non empty connected being_simple_closed_curve compact Element of K27( the U1 of (TOP-REAL 2))
len (Cage (n,C)) is V8() V12() non empty V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
{ (LSeg ((Cage (n,C)),b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Cage (n,C)) ) } is set
union { (LSeg ((Cage (n,C)),b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Cage (n,C)) ) } is set
W-min (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
W-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (n,C))) is strict SubSpace of TOP-REAL 2
proj1 | (L~ (Cage (n,C))) is V1() V4( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL))
the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))) is set
K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL) is set
K27(K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL)) is set
K406(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj1 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
W-most (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
SW-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
S-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
proj2 | (L~ (Cage (n,C))) is V1() V4( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL))
K406(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj2 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),(S-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
NW-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
N-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
K407(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj2 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),(N-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (n,C)))),(NW-corner (L~ (Cage (n,C))))) is connected compact compact Element of K27( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ (Cage (n,C)))),(NW-corner (L~ (Cage (n,C)))))) /\ (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ (Cage (n,C)))) is strict SubSpace of TOP-REAL 2
proj2 | (W-most (L~ (Cage (n,C)))) is V1() V4( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C)))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL))
the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))) is set
K28( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL) is set
K27(K28( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL)) is set
K406(((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),(proj2 | (W-most (L~ (Cage (n,C)))))) is V35() V36() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),K406(((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),(proj2 | (W-most (L~ (Cage (n,C))))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C))))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() V24() FinSequence-like FinSubsequence-like circular special unfolded V220() V221() clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
E-max (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
E-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
K407(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj1 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
E-most (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
SE-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ (Cage (n,C)))),(S-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
NE-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ (Cage (n,C)))),(N-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (n,C)))),(NE-corner (L~ (Cage (n,C))))) is connected compact compact Element of K27( the U1 of (TOP-REAL 2))
(LSeg ((SE-corner (L~ (Cage (n,C)))),(NE-corner (L~ (Cage (n,C)))))) /\ (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ (Cage (n,C)))) is strict SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (n,C)))) is V1() V4( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C)))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL))
the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))) is set
K28( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL) is set
K27(K28( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL)) is set
K407(((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),(proj2 | (E-most (L~ (Cage (n,C)))))) is V35() V36() ext-real Element of REAL
|[(E-bound (L~ (Cage (n,C)))),K407(((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),(proj2 | (E-most (L~ (Cage (n,C))))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
(Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C)))))) -: (E-max (L~ (Cage (n,C)))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like special unfolded FinSequence of the U1 of (TOP-REAL 2)
len (n,C) is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
(E-max (L~ (Cage (n,C)))) .. (Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C)))))) is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
rng (Cage (n,C)) is V19() set
rng (Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C)))))) is V19() set
n is non empty compact non horizontal non vertical Element of K27( the U1 of (TOP-REAL 2))
C is V8() V12() V24() cardinal V35() V36() ext-real set
Cage (n,C) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() V24() FinSequence-like FinSubsequence-like circular special unfolded V220() V221() clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Cage (n,C)) is non empty connected being_simple_closed_curve compact Element of K27( the U1 of (TOP-REAL 2))
len (Cage (n,C)) is V8() V12() non empty V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
{ (LSeg ((Cage (n,C)),b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Cage (n,C)) ) } is set
union { (LSeg ((Cage (n,C)),b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Cage (n,C)) ) } is set
W-min (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
W-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (n,C))) is strict SubSpace of TOP-REAL 2
proj1 | (L~ (Cage (n,C))) is V1() V4( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL))
the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))) is set
K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL) is set
K27(K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL)) is set
K406(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj1 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
W-most (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
SW-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
S-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
proj2 | (L~ (Cage (n,C))) is V1() V4( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL))
K406(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj2 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),(S-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
NW-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
N-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
K407(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj2 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),(N-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (n,C)))),(NW-corner (L~ (Cage (n,C))))) is connected compact compact Element of K27( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ (Cage (n,C)))),(NW-corner (L~ (Cage (n,C)))))) /\ (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ (Cage (n,C)))) is strict SubSpace of TOP-REAL 2
proj2 | (W-most (L~ (Cage (n,C)))) is V1() V4( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C)))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL))
the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))) is set
K28( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL) is set
K27(K28( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL)) is set
K406(((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),(proj2 | (W-most (L~ (Cage (n,C)))))) is V35() V36() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),K406(((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),(proj2 | (W-most (L~ (Cage (n,C))))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C))))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() V24() FinSequence-like FinSubsequence-like circular special unfolded V220() V221() clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
E-max (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
E-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
K407(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj1 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
E-most (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
SE-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ (Cage (n,C)))),(S-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
NE-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ (Cage (n,C)))),(N-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (n,C)))),(NE-corner (L~ (Cage (n,C))))) is connected compact compact Element of K27( the U1 of (TOP-REAL 2))
(LSeg ((SE-corner (L~ (Cage (n,C)))),(NE-corner (L~ (Cage (n,C)))))) /\ (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ (Cage (n,C)))) is strict SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (n,C)))) is V1() V4( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C)))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL))
the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))) is set
K28( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL) is set
K27(K28( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL)) is set
K407(((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),(proj2 | (E-most (L~ (Cage (n,C)))))) is V35() V36() ext-real Element of REAL
|[(E-bound (L~ (Cage (n,C)))),K407(((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),(proj2 | (E-most (L~ (Cage (n,C))))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
(Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C)))))) :- (E-max (L~ (Cage (n,C)))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n is non empty compact non horizontal non vertical Element of K27( the U1 of (TOP-REAL 2))
C is V8() V12() V24() cardinal V35() V36() ext-real set
(n,C) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Cage (n,C) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() V24() FinSequence-like FinSubsequence-like circular special unfolded V220() V221() clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Cage (n,C)) is non empty connected being_simple_closed_curve compact Element of K27( the U1 of (TOP-REAL 2))
len (Cage (n,C)) is V8() V12() non empty V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
{ (LSeg ((Cage (n,C)),b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Cage (n,C)) ) } is set
union { (LSeg ((Cage (n,C)),b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Cage (n,C)) ) } is set
W-min (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
W-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (n,C))) is strict SubSpace of TOP-REAL 2
proj1 | (L~ (Cage (n,C))) is V1() V4( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL))
the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))) is set
K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL) is set
K27(K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL)) is set
K406(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj1 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
W-most (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
SW-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
S-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
proj2 | (L~ (Cage (n,C))) is V1() V4( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL))
K406(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj2 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),(S-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
NW-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
N-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
K407(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj2 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),(N-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (n,C)))),(NW-corner (L~ (Cage (n,C))))) is connected compact compact Element of K27( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ (Cage (n,C)))),(NW-corner (L~ (Cage (n,C)))))) /\ (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ (Cage (n,C)))) is strict SubSpace of TOP-REAL 2
proj2 | (W-most (L~ (Cage (n,C)))) is V1() V4( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C)))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL))
the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))) is set
K28( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL) is set
K27(K28( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL)) is set
K406(((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),(proj2 | (W-most (L~ (Cage (n,C)))))) is V35() V36() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),K406(((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),(proj2 | (W-most (L~ (Cage (n,C))))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C))))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() V24() FinSequence-like FinSubsequence-like circular special unfolded V220() V221() clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
E-max (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
E-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
K407(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj1 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
E-most (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
SE-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ (Cage (n,C)))),(S-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
NE-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ (Cage (n,C)))),(N-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (n,C)))),(NE-corner (L~ (Cage (n,C))))) is connected compact compact Element of K27( the U1 of (TOP-REAL 2))
(LSeg ((SE-corner (L~ (Cage (n,C)))),(NE-corner (L~ (Cage (n,C)))))) /\ (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ (Cage (n,C)))) is strict SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (n,C)))) is V1() V4( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C)))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL))
the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))) is set
K28( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL) is set
K27(K28( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL)) is set
K407(((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),(proj2 | (E-most (L~ (Cage (n,C)))))) is V35() V36() ext-real Element of REAL
|[(E-bound (L~ (Cage (n,C)))),K407(((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),(proj2 | (E-most (L~ (Cage (n,C))))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
(Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C)))))) :- (E-max (L~ (Cage (n,C)))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (n,C) is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
len (Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C)))))) is V8() V12() non empty V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
(E-max (L~ (Cage (n,C)))) .. (Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C)))))) is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
(len (Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C))))))) - ((E-max (L~ (Cage (n,C)))) .. (Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C))))))) is V35() V36() ext-real set
((len (Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C))))))) - ((E-max (L~ (Cage (n,C)))) .. (Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C)))))))) + 1 is V35() V36() ext-real set
rng (Cage (n,C)) is V19() set
rng (Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C)))))) is V19() set
n is non empty compact non horizontal non vertical Element of K27( the U1 of (TOP-REAL 2))
C is V8() V12() V24() cardinal V35() V36() ext-real set
(n,C) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Cage (n,C) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() V24() FinSequence-like FinSubsequence-like circular special unfolded V220() V221() clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Cage (n,C)) is non empty connected being_simple_closed_curve compact Element of K27( the U1 of (TOP-REAL 2))
len (Cage (n,C)) is V8() V12() non empty V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT
{ (LSeg ((Cage (n,C)),b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Cage (n,C)) ) } is set
union { (LSeg ((Cage (n,C)),b₁)) where b₁ is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167() V168() V169() V170() V171() V172() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Cage (n,C)) ) } is set
W-min (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
W-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (n,C))) is strict SubSpace of TOP-REAL 2
proj1 | (L~ (Cage (n,C))) is V1() V4( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL))
the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))) is set
K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL) is set
K27(K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL)) is set
K406(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj1 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
W-most (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
SW-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
S-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
proj2 | (L~ (Cage (n,C))) is V1() V4( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL))
K406(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj2 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),(S-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
NW-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
N-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
K407(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj2 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),(N-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (n,C)))),(NW-corner (L~ (Cage (n,C))))) is connected compact compact Element of K27( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ (Cage (n,C)))),(NW-corner (L~ (Cage (n,C)))))) /\ (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ (Cage (n,C)))) is strict SubSpace of TOP-REAL 2
proj2 | (W-most (L~ (Cage (n,C)))) is V1() V4( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C)))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL))
the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))) is set
K28( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL) is set
K27(K28( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL)) is set
K406(((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),(proj2 | (W-most (L~ (Cage (n,C)))))) is V35() V36() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),K406(((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),(proj2 | (W-most (L~ (Cage (n,C))))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C))))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() V24() FinSequence-like FinSubsequence-like circular special unfolded V220() V221() clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
E-max (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
E-bound (L~ (Cage (n,C))) is V35() V36() ext-real Element of REAL
K407(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj1 | (L~ (Cage (n,C))))) is V35() V36() ext-real Element of REAL
E-most (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
SE-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ (Cage (n,C)))),(S-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
NE-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V159() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ (Cage (n,C)))),(N-bound (L~ (Cage (n,C))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (n,C)))),(NE-corner (L~ (Cage (n,C))))) is connected compact compact Element of K27( the U1 of (TOP-REAL 2))
(LSeg ((SE-corner (L~ (Cage (n,C)))),(NE-corner (L~ (Cage (n,C)))))) /\ (L~ (Cage (n,C))) is Element of K27( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ (Cage (n,C)))) is strict SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (n,C)))) is V1() V4( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C)))))) V5( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))), REAL ) Element of K27(K28( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL))
the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))) is set
K28( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL) is set
K27(K28( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL)) is set
K407(((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),(proj2 | (E-most (L~ (Cage (n,C)))))) is V35() V36() ext-real Element of REAL
|[(E-bound (L~ (Cage (n,C)))),K407(((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),(proj2 | (E-most (L~ (Cage (n,C))))))]| is V1() V4( NAT ) Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like V159() Element of the U1 of (TOP-REAL 2)
(Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C)))))) -: (E-max (L~ (Cage (n,C)))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like special unfolded FinSequence of the U1 of (TOP-REAL 2)
rng (Cage (n,C)) is V19() set
rng (Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C)))))) is V19() set
len (n,C) is V8() V12() V24() cardinal V35() V36() V37() ext-real V156() V167()