:: 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

union { (LSeg (C,b

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

union { (LSeg (C,b

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

union { (LSeg (n,b

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

union { (LSeg (n,b

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

union { (LSeg ((R_Cut (n,C)),b

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

union { (LSeg (n,b

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

union { (LSeg ((mid (n,((Index (C,n)) + 1),(len n))),b

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

union { (LSeg (n,b

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

union { (LSeg ((L_Cut (n,C)),b

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

union { (LSeg ((mid (n,((Index (C,n)) + 1),(len n))),b

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

union { (LSeg ((Cage (n,C)),b

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

union { (LSeg ((Cage (n,C)),b

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

union { (LSeg ((Cage (n,C)),b

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

union { (LSeg ((Cage (n,C)),b

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

union { (LSeg ((Cage (n,C)),b

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()