REAL is V138() V139() V140() V144() set
NAT is V138() V139() V140() V141() V142() V143() V144() Element of K6(REAL)
K6(REAL) is set
NAT is V138() V139() V140() V141() V142() V143() V144() set
K6(NAT) is set
K6(NAT) is set
COMPLEX is V138() V144() set
1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
K7(1,1) is set
K6(K7(1,1)) is set
K7(K7(1,1),1) is set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
K7(2,2) is set
K7(K7(2,2),REAL) is set
K6(K7(K7(2,2),REAL)) is set
RAT is V138() V139() V140() V141() V144() set
INT is V138() V139() V140() V141() V142() V144() set
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like V104() V150() V151() V152() V153() V154() V155() V156() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
K6( the carrier of (TOP-REAL 2)) is set
K337( the carrier of (TOP-REAL 2)) is M11( the carrier of (TOP-REAL 2))
K7(COMPLEX,COMPLEX) is set
K6(K7(COMPLEX,COMPLEX)) is set
K7(COMPLEX,REAL) is set
K6(K7(COMPLEX,REAL)) is set
K7( the carrier of (TOP-REAL 2),REAL) is set
K6(K7( the carrier of (TOP-REAL 2),REAL)) is set
{} is empty Function-like functional V138() V139() V140() V141() V142() V143() V144() set
3 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
4 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
0 is empty V6() V10() V11() V12() Function-like functional V37() ext-real non positive non negative V76() V138() V139() V140() V141() V142() V143() V144() Element of NAT
K74({}) is set
rng {} is set
Seg 1 is V138() V139() V140() V141() V142() V143() Element of K6(NAT)
proj2 is V13() V16( the carrier of (TOP-REAL 2)) V17( REAL ) Function-like V40( the carrier of (TOP-REAL 2), REAL ) V197( TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
i is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
C is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[i,C] is set
{i,C} is non empty V138() V139() V140() V141() V142() V143() set
{i} is non empty V138() V139() V140() V141() V142() V143() set
{{i,C},{i}} is non empty set
p is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[i,p] is set
{i,p} is non empty V138() V139() V140() V141() V142() V143() set
{{i,p},{i}} is non empty set
k is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ k is compact Element of K6( the carrier of (TOP-REAL 2))
l is V13() non empty-yielding V16( NAT ) V17(K337( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K337( the carrier of (TOP-REAL 2))
l * (i,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l * (i,p) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((l * (i,C)),(l * (i,p))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
Indices l is set
(LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k) is compact Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V138() V139() V140() Element of K6(REAL)
lower_bound (proj2 .: ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is V11() V12() ext-real Element of REAL
len l is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
n is set
f is non empty compact Element of K6( the carrier of (TOP-REAL 2))
S-most f is non empty compact Element of K6( the carrier of (TOP-REAL 2))
SW-corner f is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
W-bound f is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | f is strict compact SubSpace of TOP-REAL 2
proj1 is V13() V16( the carrier of (TOP-REAL 2)) V17( REAL ) Function-like V40( the carrier of (TOP-REAL 2), REAL ) V197( TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
proj1 | f is V13() V16( the carrier of ((TOP-REAL 2) | f)) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | f), REAL ) V197((TOP-REAL 2) | f) Element of K6(K7( the carrier of ((TOP-REAL 2) | f),REAL))
the carrier of ((TOP-REAL 2) | f) is set
K7( the carrier of ((TOP-REAL 2) | f),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | f),REAL)) is set
lower_bound (proj1 | f) is V11() V12() ext-real Element of REAL
(proj1 | f) .: the carrier of ((TOP-REAL 2) | f) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() V12() ext-real Element of REAL
S-bound f is V11() V12() ext-real Element of REAL
proj2 | f is V13() V16( the carrier of ((TOP-REAL 2) | f)) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | f), REAL ) V197((TOP-REAL 2) | f) Element of K6(K7( the carrier of ((TOP-REAL 2) | f),REAL))
lower_bound (proj2 | f) is V11() V12() ext-real Element of REAL
(proj2 | f) .: the carrier of ((TOP-REAL 2) | f) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() V12() ext-real Element of REAL
|[(W-bound f),(S-bound f)]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
SE-corner f is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
E-bound f is V11() V12() ext-real Element of REAL
upper_bound (proj1 | f) is V11() V12() ext-real Element of REAL
upper_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() V12() ext-real Element of REAL
|[(E-bound f),(S-bound f)]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SW-corner f),(SE-corner f)) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SW-corner f),(SE-corner f))) /\ f is compact Element of K6( the carrier of (TOP-REAL 2))
n is set
c9 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is strict SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is set
proj2 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V13() V16( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))), REAL ) V197((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) Element of K6(K7( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))),REAL))
K7( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))),REAL)) is set
(proj2 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) .: ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V138() V139() V140() Element of K6(REAL)
[#] ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is non proper Element of K6( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))))
K6( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) is set
(proj2 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) .: ([#] ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) .: ([#] ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))))) is V11() V12() ext-real Element of REAL
S-bound ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V11() V12() ext-real Element of REAL
lower_bound (proj2 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is V11() V12() ext-real Element of REAL
(proj2 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) is V11() V12() ext-real Element of REAL
c9 `2 is V11() V12() ext-real Element of REAL
S-min ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
S-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is Element of K6( the carrier of (TOP-REAL 2))
SW-corner ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
W-bound ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V11() V12() ext-real Element of REAL
proj1 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V13() V16( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))), REAL ) V197((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) Element of K6(K7( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))),REAL))
lower_bound (proj1 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is V11() V12() ext-real Element of REAL
(proj1 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj1 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) is V11() V12() ext-real Element of REAL
|[(W-bound ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))),(S-bound ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
SE-corner ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
E-bound ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V11() V12() ext-real Element of REAL
upper_bound (proj1 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is V11() V12() ext-real Element of REAL
upper_bound ((proj1 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) is V11() V12() ext-real Element of REAL
|[(E-bound ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))),(S-bound ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SW-corner ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))),(SE-corner ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SW-corner ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))),(SE-corner ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))))) /\ ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (S-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is strict SubSpace of TOP-REAL 2
proj1 | (S-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is V13() V16( the carrier of ((TOP-REAL 2) | (S-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (S-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))), REAL ) V197((TOP-REAL 2) | (S-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (S-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))),REAL))
the carrier of ((TOP-REAL 2) | (S-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) is set
K7( the carrier of ((TOP-REAL 2) | (S-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (S-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))),REAL)) is set
lower_bound (proj1 | (S-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) is V11() V12() ext-real Element of REAL
(proj1 | (S-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) .: the carrier of ((TOP-REAL 2) | (S-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj1 | (S-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) .: the carrier of ((TOP-REAL 2) | (S-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))))) is V11() V12() ext-real Element of REAL
|[(lower_bound (proj1 | (S-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))))),(S-bound ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(S-min ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) `2 is V11() V12() ext-real Element of REAL
width l is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(l * (i,C)) `2 is V11() V12() ext-real Element of REAL
(l * (i,p)) `2 is V11() V12() ext-real Element of REAL
(l * (i,C)) `1 is V11() V12() ext-real Element of REAL
l * (i,1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (i,1)) `1 is V11() V12() ext-real Element of REAL
(l * (i,p)) `1 is V11() V12() ext-real Element of REAL
len k is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
{ (LSeg (k,b1)) where b1 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT : ( 1 <= b1 & b1 + 1 <= len k ) } is set
union { (LSeg (k,b1)) where b1 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT : ( 1 <= b1 & b1 + 1 <= len k ) } is set
j2 is set
i1 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
LSeg (k,i1) is Element of K6( the carrier of (TOP-REAL 2))
i1 + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
k /. i1 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
k /. (i1 + 1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((k /. i1),(k /. (i1 + 1))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
Seg (len k) is V138() V139() V140() V141() V142() V143() Element of K6(NAT)
dom k is V138() V139() V140() V141() V142() V143() Element of K6(NAT)
jo is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
io is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[jo,io] is set
{jo,io} is non empty V138() V139() V140() V141() V142() V143() set
{jo} is non empty V138() V139() V140() V141() V142() V143() set
{{jo,io},{jo}} is non empty set
l * (jo,io) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
j0 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
i0 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[j0,i0] is set
{j0,i0} is non empty V138() V139() V140() V141() V142() V143() set
{j0} is non empty V138() V139() V140() V141() V142() V143() set
{{j0,i0},{j0}} is non empty set
l * (j0,i0) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(k /. i1) `1 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `1 is V11() V12() ext-real Element of REAL
l * (jo,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (jo,C)) `1 is V11() V12() ext-real Element of REAL
l * (jo,1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (jo,1)) `1 is V11() V12() ext-real Element of REAL
(l * (jo,io)) `1 is V11() V12() ext-real Element of REAL
c9 `1 is V11() V12() ext-real Element of REAL
l * (j0,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (j0,C)) `1 is V11() V12() ext-real Element of REAL
l * (j0,1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (j0,1)) `1 is V11() V12() ext-real Element of REAL
(l * (j0,i0)) `1 is V11() V12() ext-real Element of REAL
(k /. i1) `2 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `2 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (i,n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l * (1,i0) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (1,i0)) `2 is V11() V12() ext-real Element of REAL
(l * (i,n)) `2 is V11() V12() ext-real Element of REAL
(l * (i,n)) `1 is V11() V12() ext-real Element of REAL
(l * (jo,io)) `2 is V11() V12() ext-real Element of REAL
l * (1,io) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (1,io)) `2 is V11() V12() ext-real Element of REAL
l * (i,io) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (i,io)) `2 is V11() V12() ext-real Element of REAL
j0 - jo is V11() V12() ext-real set
abs (j0 - jo) is V11() V12() ext-real Element of REAL
i0 - io is V11() V12() ext-real set
abs (i0 - io) is V11() V12() ext-real Element of REAL
(abs (j0 - jo)) + (abs (i0 - io)) is V11() V12() ext-real set
0 + (abs (i0 - io)) is V11() V12() ext-real set
- (i0 - io) is V11() V12() ext-real set
abs (- (i0 - io)) is V11() V12() ext-real Element of REAL
io + 0 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
io - i0 is V11() V12() ext-real set
i0 + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (i,i0) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (i,i0)) `2 is V11() V12() ext-real Element of REAL
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (i,n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (i,n)) `1 is V11() V12() ext-real Element of REAL
(k /. i1) `2 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `2 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (i,n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l * (1,io) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (1,io)) `2 is V11() V12() ext-real Element of REAL
(l * (i,n)) `2 is V11() V12() ext-real Element of REAL
(l * (i,n)) `1 is V11() V12() ext-real Element of REAL
(l * (j0,i0)) `2 is V11() V12() ext-real Element of REAL
l * (1,i0) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (1,i0)) `2 is V11() V12() ext-real Element of REAL
l * (i,i0) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (i,i0)) `2 is V11() V12() ext-real Element of REAL
i0 + 0 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
io - i0 is V11() V12() ext-real set
- 0 is empty V11() V12() Function-like functional ext-real non positive non negative V138() V139() V140() V141() V142() V143() V144() set
- (io - i0) is V11() V12() ext-real set
j0 - jo is V11() V12() ext-real set
abs (j0 - jo) is V11() V12() ext-real Element of REAL
i0 - io is V11() V12() ext-real set
abs (i0 - io) is V11() V12() ext-real Element of REAL
(abs (j0 - jo)) + (abs (i0 - io)) is V11() V12() ext-real set
0 + (abs (i0 - io)) is V11() V12() ext-real set
io + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
i0 - 0 is V11() V12() ext-real non negative set
l * (i,io) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (i,io)) `2 is V11() V12() ext-real Element of REAL
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (i,n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (i,n)) `1 is V11() V12() ext-real Element of REAL
(k /. i1) `2 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `2 is V11() V12() ext-real Element of REAL
(k /. i1) `2 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `2 is V11() V12() ext-real Element of REAL
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (i,n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l * (1,i0) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (1,i0)) `2 is V11() V12() ext-real Element of REAL
(l * (i,n)) `2 is V11() V12() ext-real Element of REAL
c9 `1 is V11() V12() ext-real Element of REAL
(l * (i,n)) `1 is V11() V12() ext-real Element of REAL
(k /. i1) `1 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `1 is V11() V12() ext-real Element of REAL
(k /. i1) `2 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `2 is V11() V12() ext-real Element of REAL
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (i,n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
i is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
C is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[i,C] is set
{i,C} is non empty V138() V139() V140() V141() V142() V143() set
{i} is non empty V138() V139() V140() V141() V142() V143() set
{{i,C},{i}} is non empty set
p is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[i,p] is set
{i,p} is non empty V138() V139() V140() V141() V142() V143() set
{{i,p},{i}} is non empty set
k is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ k is compact Element of K6( the carrier of (TOP-REAL 2))
l is V13() non empty-yielding V16( NAT ) V17(K337( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K337( the carrier of (TOP-REAL 2))
l * (i,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l * (i,p) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((l * (i,C)),(l * (i,p))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
Indices l is set
(LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k) is compact Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V138() V139() V140() Element of K6(REAL)
upper_bound (proj2 .: ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is V11() V12() ext-real Element of REAL
len l is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
n is set
f is non empty compact Element of K6( the carrier of (TOP-REAL 2))
N-most f is non empty compact Element of K6( the carrier of (TOP-REAL 2))
NW-corner f is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
W-bound f is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | f is strict compact SubSpace of TOP-REAL 2
proj1 is V13() V16( the carrier of (TOP-REAL 2)) V17( REAL ) Function-like V40( the carrier of (TOP-REAL 2), REAL ) V197( TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
proj1 | f is V13() V16( the carrier of ((TOP-REAL 2) | f)) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | f), REAL ) V197((TOP-REAL 2) | f) Element of K6(K7( the carrier of ((TOP-REAL 2) | f),REAL))
the carrier of ((TOP-REAL 2) | f) is set
K7( the carrier of ((TOP-REAL 2) | f),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | f),REAL)) is set
lower_bound (proj1 | f) is V11() V12() ext-real Element of REAL
(proj1 | f) .: the carrier of ((TOP-REAL 2) | f) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() V12() ext-real Element of REAL
N-bound f is V11() V12() ext-real Element of REAL
proj2 | f is V13() V16( the carrier of ((TOP-REAL 2) | f)) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | f), REAL ) V197((TOP-REAL 2) | f) Element of K6(K7( the carrier of ((TOP-REAL 2) | f),REAL))
upper_bound (proj2 | f) is V11() V12() ext-real Element of REAL
(proj2 | f) .: the carrier of ((TOP-REAL 2) | f) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj2 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() V12() ext-real Element of REAL
|[(W-bound f),(N-bound f)]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NE-corner f is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
E-bound f is V11() V12() ext-real Element of REAL
upper_bound (proj1 | f) is V11() V12() ext-real Element of REAL
upper_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() V12() ext-real Element of REAL
|[(E-bound f),(N-bound f)]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((NW-corner f),(NE-corner f)) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((NW-corner f),(NE-corner f))) /\ f is compact Element of K6( the carrier of (TOP-REAL 2))
n is set
c9 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
len k is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
{ (LSeg (k,b1)) where b1 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT : ( 1 <= b1 & b1 + 1 <= len k ) } is set
union { (LSeg (k,b1)) where b1 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT : ( 1 <= b1 & b1 + 1 <= len k ) } is set
j2 is set
i1 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
LSeg (k,i1) is Element of K6( the carrier of (TOP-REAL 2))
i1 + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
k /. i1 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
k /. (i1 + 1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((k /. i1),(k /. (i1 + 1))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is strict SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is set
proj2 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V13() V16( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))), REAL ) V197((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) Element of K6(K7( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))),REAL))
K7( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))),REAL)) is set
(proj2 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) .: ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V138() V139() V140() Element of K6(REAL)
[#] ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is non proper Element of K6( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))))
K6( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) is set
(proj2 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) .: ([#] ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj2 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) .: ([#] ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))))) is V11() V12() ext-real Element of REAL
N-bound ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V11() V12() ext-real Element of REAL
upper_bound (proj2 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is V11() V12() ext-real Element of REAL
(proj2 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj2 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) is V11() V12() ext-real Element of REAL
Seg (len k) is V138() V139() V140() V141() V142() V143() Element of K6(NAT)
dom k is V138() V139() V140() V141() V142() V143() Element of K6(NAT)
jo is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
io is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[jo,io] is set
{jo,io} is non empty V138() V139() V140() V141() V142() V143() set
{jo} is non empty V138() V139() V140() V141() V142() V143() set
{{jo,io},{jo}} is non empty set
l * (jo,io) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
c9 `2 is V11() V12() ext-real Element of REAL
N-min ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
N-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is Element of K6( the carrier of (TOP-REAL 2))
NW-corner ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
W-bound ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V11() V12() ext-real Element of REAL
proj1 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V13() V16( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))), REAL ) V197((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) Element of K6(K7( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))),REAL))
lower_bound (proj1 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is V11() V12() ext-real Element of REAL
(proj1 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj1 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) is V11() V12() ext-real Element of REAL
|[(W-bound ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))),(N-bound ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NE-corner ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
E-bound ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is V11() V12() ext-real Element of REAL
upper_bound (proj1 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is V11() V12() ext-real Element of REAL
upper_bound ((proj1 | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) is V11() V12() ext-real Element of REAL
|[(E-bound ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))),(N-bound ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((NW-corner ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))),(NE-corner ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((NW-corner ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))),(NE-corner ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))))) /\ ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (N-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is strict SubSpace of TOP-REAL 2
proj1 | (N-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) is V13() V16( the carrier of ((TOP-REAL 2) | (N-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (N-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))), REAL ) V197((TOP-REAL 2) | (N-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (N-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))),REAL))
the carrier of ((TOP-REAL 2) | (N-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) is set
K7( the carrier of ((TOP-REAL 2) | (N-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (N-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))),REAL)) is set
lower_bound (proj1 | (N-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) is V11() V12() ext-real Element of REAL
(proj1 | (N-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) .: the carrier of ((TOP-REAL 2) | (N-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj1 | (N-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))) .: the carrier of ((TOP-REAL 2) | (N-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))))) is V11() V12() ext-real Element of REAL
|[(lower_bound (proj1 | (N-most ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))))),(N-bound ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k)))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(N-min ((LSeg ((l * (i,C)),(l * (i,p)))) /\ (L~ k))) `2 is V11() V12() ext-real Element of REAL
width l is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(l * (i,C)) `2 is V11() V12() ext-real Element of REAL
(l * (i,p)) `2 is V11() V12() ext-real Element of REAL
(l * (i,C)) `1 is V11() V12() ext-real Element of REAL
l * (i,1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (i,1)) `1 is V11() V12() ext-real Element of REAL
(l * (i,p)) `1 is V11() V12() ext-real Element of REAL
j0 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
i0 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[j0,i0] is set
{j0,i0} is non empty V138() V139() V140() V141() V142() V143() set
{j0} is non empty V138() V139() V140() V141() V142() V143() set
{{j0,i0},{j0}} is non empty set
l * (j0,i0) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(k /. i1) `1 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `1 is V11() V12() ext-real Element of REAL
l * (jo,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (jo,C)) `1 is V11() V12() ext-real Element of REAL
l * (jo,1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (jo,1)) `1 is V11() V12() ext-real Element of REAL
(l * (jo,io)) `1 is V11() V12() ext-real Element of REAL
c9 `1 is V11() V12() ext-real Element of REAL
l * (j0,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (j0,C)) `1 is V11() V12() ext-real Element of REAL
l * (j0,1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (j0,1)) `1 is V11() V12() ext-real Element of REAL
(l * (j0,i0)) `1 is V11() V12() ext-real Element of REAL
(k /. i1) `2 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `2 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (i,n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l * (1,io) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (1,io)) `2 is V11() V12() ext-real Element of REAL
(l * (i,n)) `2 is V11() V12() ext-real Element of REAL
(l * (i,n)) `1 is V11() V12() ext-real Element of REAL
(l * (j0,i0)) `2 is V11() V12() ext-real Element of REAL
l * (1,i0) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (1,i0)) `2 is V11() V12() ext-real Element of REAL
l * (i,i0) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (i,i0)) `2 is V11() V12() ext-real Element of REAL
j0 - jo is V11() V12() ext-real set
abs (j0 - jo) is V11() V12() ext-real Element of REAL
i0 - io is V11() V12() ext-real set
abs (i0 - io) is V11() V12() ext-real Element of REAL
(abs (j0 - jo)) + (abs (i0 - io)) is V11() V12() ext-real set
0 + (abs (i0 - io)) is V11() V12() ext-real set
- (i0 - io) is V11() V12() ext-real set
abs (- (i0 - io)) is V11() V12() ext-real Element of REAL
io + 0 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
io - i0 is V11() V12() ext-real set
i0 + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (i,io) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (i,io)) `2 is V11() V12() ext-real Element of REAL
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (i,n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (i,n)) `1 is V11() V12() ext-real Element of REAL
(k /. i1) `2 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `2 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (i,n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l * (1,i0) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (1,i0)) `2 is V11() V12() ext-real Element of REAL
(l * (i,n)) `2 is V11() V12() ext-real Element of REAL
(l * (i,n)) `1 is V11() V12() ext-real Element of REAL
(l * (jo,io)) `2 is V11() V12() ext-real Element of REAL
l * (1,io) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (1,io)) `2 is V11() V12() ext-real Element of REAL
l * (i,io) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (i,io)) `2 is V11() V12() ext-real Element of REAL
i0 + 0 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
io - i0 is V11() V12() ext-real set
- 0 is empty V11() V12() Function-like functional ext-real non positive non negative V138() V139() V140() V141() V142() V143() V144() set
- (io - i0) is V11() V12() ext-real set
j0 - jo is V11() V12() ext-real set
abs (j0 - jo) is V11() V12() ext-real Element of REAL
i0 - io is V11() V12() ext-real set
abs (i0 - io) is V11() V12() ext-real Element of REAL
(abs (j0 - jo)) + (abs (i0 - io)) is V11() V12() ext-real set
0 + (abs (i0 - io)) is V11() V12() ext-real set
io + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
i0 - 0 is V11() V12() ext-real non negative set
l * (i,i0) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (i,i0)) `2 is V11() V12() ext-real Element of REAL
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (i,n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (i,n)) `1 is V11() V12() ext-real Element of REAL
(k /. i1) `2 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `2 is V11() V12() ext-real Element of REAL
(k /. i1) `2 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `2 is V11() V12() ext-real Element of REAL
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (i,n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l * (1,i0) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (1,i0)) `2 is V11() V12() ext-real Element of REAL
(l * (i,n)) `2 is V11() V12() ext-real Element of REAL
c9 `1 is V11() V12() ext-real Element of REAL
(l * (i,n)) `1 is V11() V12() ext-real Element of REAL
(k /. i1) `1 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `1 is V11() V12() ext-real Element of REAL
(k /. i1) `2 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `2 is V11() V12() ext-real Element of REAL
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (i,n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
proj1 is V13() V16( the carrier of (TOP-REAL 2)) V17( REAL ) Function-like V40( the carrier of (TOP-REAL 2), REAL ) V197( TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
i is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
C is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[i,C] is set
{i,C} is non empty V138() V139() V140() V141() V142() V143() set
{i} is non empty V138() V139() V140() V141() V142() V143() set
{{i,C},{i}} is non empty set
p is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[p,C] is set
{p,C} is non empty V138() V139() V140() V141() V142() V143() set
{p} is non empty V138() V139() V140() V141() V142() V143() set
{{p,C},{p}} is non empty set
k is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ k is compact Element of K6( the carrier of (TOP-REAL 2))
l is V13() non empty-yielding V16( NAT ) V17(K337( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K337( the carrier of (TOP-REAL 2))
l * (i,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l * (p,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((l * (i,C)),(l * (p,C))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
Indices l is set
(LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k) is compact Element of K6( the carrier of (TOP-REAL 2))
proj1 .: ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V138() V139() V140() Element of K6(REAL)
lower_bound (proj1 .: ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is V11() V12() ext-real Element of REAL
n is set
f is non empty compact Element of K6( the carrier of (TOP-REAL 2))
W-most f is non empty compact Element of K6( the carrier of (TOP-REAL 2))
SW-corner f is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
W-bound f is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | f is strict compact SubSpace of TOP-REAL 2
proj1 | f is V13() V16( the carrier of ((TOP-REAL 2) | f)) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | f), REAL ) V197((TOP-REAL 2) | f) Element of K6(K7( the carrier of ((TOP-REAL 2) | f),REAL))
the carrier of ((TOP-REAL 2) | f) is set
K7( the carrier of ((TOP-REAL 2) | f),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | f),REAL)) is set
lower_bound (proj1 | f) is V11() V12() ext-real Element of REAL
(proj1 | f) .: the carrier of ((TOP-REAL 2) | f) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() V12() ext-real Element of REAL
S-bound f is V11() V12() ext-real Element of REAL
proj2 | f is V13() V16( the carrier of ((TOP-REAL 2) | f)) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | f), REAL ) V197((TOP-REAL 2) | f) Element of K6(K7( the carrier of ((TOP-REAL 2) | f),REAL))
lower_bound (proj2 | f) is V11() V12() ext-real Element of REAL
(proj2 | f) .: the carrier of ((TOP-REAL 2) | f) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() V12() ext-real Element of REAL
|[(W-bound f),(S-bound f)]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NW-corner f is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
N-bound f is V11() V12() ext-real Element of REAL
upper_bound (proj2 | f) is V11() V12() ext-real Element of REAL
upper_bound ((proj2 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() V12() ext-real Element of REAL
|[(W-bound f),(N-bound f)]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SW-corner f),(NW-corner f)) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SW-corner f),(NW-corner f))) /\ f is compact Element of K6( the carrier of (TOP-REAL 2))
n is set
c9 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is strict SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is set
proj1 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V13() V16( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))), REAL ) V197((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) Element of K6(K7( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))),REAL))
K7( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))),REAL)) is set
(proj1 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) .: ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V138() V139() V140() Element of K6(REAL)
[#] ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is non proper Element of K6( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))))
K6( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) is set
(proj1 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) .: ([#] ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj1 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) .: ([#] ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))))) is V11() V12() ext-real Element of REAL
W-bound ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V11() V12() ext-real Element of REAL
lower_bound (proj1 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is V11() V12() ext-real Element of REAL
(proj1 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj1 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) is V11() V12() ext-real Element of REAL
c9 `1 is V11() V12() ext-real Element of REAL
W-min ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
W-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is Element of K6( the carrier of (TOP-REAL 2))
SW-corner ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
S-bound ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V11() V12() ext-real Element of REAL
proj2 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V13() V16( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))), REAL ) V197((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) Element of K6(K7( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))),REAL))
lower_bound (proj2 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is V11() V12() ext-real Element of REAL
(proj2 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) is V11() V12() ext-real Element of REAL
|[(W-bound ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))),(S-bound ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NW-corner ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
N-bound ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V11() V12() ext-real Element of REAL
upper_bound (proj2 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is V11() V12() ext-real Element of REAL
upper_bound ((proj2 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) is V11() V12() ext-real Element of REAL
|[(W-bound ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))),(N-bound ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SW-corner ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))),(NW-corner ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SW-corner ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))),(NW-corner ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))))) /\ ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (W-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is strict SubSpace of TOP-REAL 2
proj2 | (W-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is V13() V16( the carrier of ((TOP-REAL 2) | (W-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (W-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))), REAL ) V197((TOP-REAL 2) | (W-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))),REAL))
the carrier of ((TOP-REAL 2) | (W-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) is set
K7( the carrier of ((TOP-REAL 2) | (W-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (W-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))),REAL)) is set
lower_bound (proj2 | (W-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) is V11() V12() ext-real Element of REAL
(proj2 | (W-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) .: the carrier of ((TOP-REAL 2) | (W-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | (W-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) .: the carrier of ((TOP-REAL 2) | (W-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))))) is V11() V12() ext-real Element of REAL
|[(W-bound ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))),(lower_bound (proj2 | (W-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(W-min ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) `1 is V11() V12() ext-real Element of REAL
width l is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
len l is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(l * (i,C)) `1 is V11() V12() ext-real Element of REAL
(l * (p,C)) `1 is V11() V12() ext-real Element of REAL
(l * (i,C)) `2 is V11() V12() ext-real Element of REAL
l * (1,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (1,C)) `2 is V11() V12() ext-real Element of REAL
(l * (p,C)) `2 is V11() V12() ext-real Element of REAL
len k is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
{ (LSeg (k,b1)) where b1 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT : ( 1 <= b1 & b1 + 1 <= len k ) } is set
union { (LSeg (k,b1)) where b1 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT : ( 1 <= b1 & b1 + 1 <= len k ) } is set
j2 is set
i1 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
LSeg (k,i1) is Element of K6( the carrier of (TOP-REAL 2))
i1 + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
k /. i1 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
k /. (i1 + 1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((k /. i1),(k /. (i1 + 1))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
Seg (len k) is V138() V139() V140() V141() V142() V143() Element of K6(NAT)
dom k is V138() V139() V140() V141() V142() V143() Element of K6(NAT)
jo is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
io is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[jo,io] is set
{jo,io} is non empty V138() V139() V140() V141() V142() V143() set
{jo} is non empty V138() V139() V140() V141() V142() V143() set
{{jo,io},{jo}} is non empty set
l * (jo,io) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
j0 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
i0 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[j0,i0] is set
{j0,i0} is non empty V138() V139() V140() V141() V142() V143() set
{j0} is non empty V138() V139() V140() V141() V142() V143() set
{{j0,i0},{j0}} is non empty set
l * (j0,i0) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(k /. i1) `2 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `2 is V11() V12() ext-real Element of REAL
l * (i,io) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (i,io)) `2 is V11() V12() ext-real Element of REAL
l * (1,io) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (1,io)) `2 is V11() V12() ext-real Element of REAL
(l * (jo,io)) `2 is V11() V12() ext-real Element of REAL
c9 `2 is V11() V12() ext-real Element of REAL
l * (i,i0) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (i,i0)) `2 is V11() V12() ext-real Element of REAL
l * (1,i0) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (1,i0)) `2 is V11() V12() ext-real Element of REAL
(l * (j0,i0)) `2 is V11() V12() ext-real Element of REAL
(k /. i1) `1 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `1 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (n,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l * (j0,1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (j0,1)) `1 is V11() V12() ext-real Element of REAL
(l * (n,C)) `1 is V11() V12() ext-real Element of REAL
(l * (n,C)) `2 is V11() V12() ext-real Element of REAL
(l * (jo,io)) `1 is V11() V12() ext-real Element of REAL
l * (jo,1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (jo,1)) `1 is V11() V12() ext-real Element of REAL
l * (jo,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (jo,C)) `1 is V11() V12() ext-real Element of REAL
i0 - io is V11() V12() ext-real set
abs (i0 - io) is V11() V12() ext-real Element of REAL
j0 - jo is V11() V12() ext-real set
abs (j0 - jo) is V11() V12() ext-real Element of REAL
(abs (i0 - io)) + (abs (j0 - jo)) is V11() V12() ext-real set
0 + (abs (j0 - jo)) is V11() V12() ext-real set
- (j0 - jo) is V11() V12() ext-real set
abs (- (j0 - jo)) is V11() V12() ext-real Element of REAL
jo + 0 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
jo - j0 is V11() V12() ext-real set
j0 + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (j0,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (j0,C)) `1 is V11() V12() ext-real Element of REAL
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (n,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (n,C)) `2 is V11() V12() ext-real Element of REAL
(k /. i1) `1 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `1 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (n,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l * (jo,1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (jo,1)) `1 is V11() V12() ext-real Element of REAL
(l * (n,C)) `1 is V11() V12() ext-real Element of REAL
(l * (n,C)) `2 is V11() V12() ext-real Element of REAL
(l * (j0,i0)) `1 is V11() V12() ext-real Element of REAL
l * (j0,1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (j0,1)) `1 is V11() V12() ext-real Element of REAL
l * (j0,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (j0,C)) `1 is V11() V12() ext-real Element of REAL
j0 + 0 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
jo - j0 is V11() V12() ext-real set
- 0 is empty V11() V12() Function-like functional ext-real non positive non negative V138() V139() V140() V141() V142() V143() V144() set
- (jo - j0) is V11() V12() ext-real set
i0 - io is V11() V12() ext-real set
abs (i0 - io) is V11() V12() ext-real Element of REAL
j0 - jo is V11() V12() ext-real set
abs (j0 - jo) is V11() V12() ext-real Element of REAL
(abs (i0 - io)) + (abs (j0 - jo)) is V11() V12() ext-real set
0 + (abs (j0 - jo)) is V11() V12() ext-real set
jo + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
j0 - 0 is V11() V12() ext-real non negative set
l * (jo,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (jo,C)) `1 is V11() V12() ext-real Element of REAL
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (n,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (n,C)) `2 is V11() V12() ext-real Element of REAL
(k /. i1) `1 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `1 is V11() V12() ext-real Element of REAL
(k /. i1) `1 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `1 is V11() V12() ext-real Element of REAL
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (n,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l * (j0,1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (j0,1)) `1 is V11() V12() ext-real Element of REAL
(l * (n,C)) `1 is V11() V12() ext-real Element of REAL
c9 `2 is V11() V12() ext-real Element of REAL
(l * (n,C)) `2 is V11() V12() ext-real Element of REAL
(k /. i1) `2 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `2 is V11() V12() ext-real Element of REAL
(k /. i1) `1 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `1 is V11() V12() ext-real Element of REAL
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (n,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
i is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
C is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[i,C] is set
{i,C} is non empty V138() V139() V140() V141() V142() V143() set
{i} is non empty V138() V139() V140() V141() V142() V143() set
{{i,C},{i}} is non empty set
p is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[p,C] is set
{p,C} is non empty V138() V139() V140() V141() V142() V143() set
{p} is non empty V138() V139() V140() V141() V142() V143() set
{{p,C},{p}} is non empty set
k is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ k is compact Element of K6( the carrier of (TOP-REAL 2))
l is V13() non empty-yielding V16( NAT ) V17(K337( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K337( the carrier of (TOP-REAL 2))
l * (i,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l * (p,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((l * (i,C)),(l * (p,C))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
Indices l is set
(LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k) is compact Element of K6( the carrier of (TOP-REAL 2))
proj1 .: ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V138() V139() V140() Element of K6(REAL)
upper_bound (proj1 .: ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is V11() V12() ext-real Element of REAL
n is set
f is non empty compact Element of K6( the carrier of (TOP-REAL 2))
E-most f is non empty compact Element of K6( the carrier of (TOP-REAL 2))
SE-corner f is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
E-bound f is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | f is strict compact SubSpace of TOP-REAL 2
proj1 | f is V13() V16( the carrier of ((TOP-REAL 2) | f)) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | f), REAL ) V197((TOP-REAL 2) | f) Element of K6(K7( the carrier of ((TOP-REAL 2) | f),REAL))
the carrier of ((TOP-REAL 2) | f) is set
K7( the carrier of ((TOP-REAL 2) | f),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | f),REAL)) is set
upper_bound (proj1 | f) is V11() V12() ext-real Element of REAL
(proj1 | f) .: the carrier of ((TOP-REAL 2) | f) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() V12() ext-real Element of REAL
S-bound f is V11() V12() ext-real Element of REAL
proj2 | f is V13() V16( the carrier of ((TOP-REAL 2) | f)) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | f), REAL ) V197((TOP-REAL 2) | f) Element of K6(K7( the carrier of ((TOP-REAL 2) | f),REAL))
lower_bound (proj2 | f) is V11() V12() ext-real Element of REAL
(proj2 | f) .: the carrier of ((TOP-REAL 2) | f) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() V12() ext-real Element of REAL
|[(E-bound f),(S-bound f)]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NE-corner f is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
N-bound f is V11() V12() ext-real Element of REAL
upper_bound (proj2 | f) is V11() V12() ext-real Element of REAL
upper_bound ((proj2 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() V12() ext-real Element of REAL
|[(E-bound f),(N-bound f)]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SE-corner f),(NE-corner f)) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SE-corner f),(NE-corner f))) /\ f is compact Element of K6( the carrier of (TOP-REAL 2))
n is set
c9 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is strict SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is set
proj1 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V13() V16( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))), REAL ) V197((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) Element of K6(K7( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))),REAL))
K7( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))),REAL)) is set
(proj1 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) .: ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V138() V139() V140() Element of K6(REAL)
[#] ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is non proper Element of K6( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))))
K6( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) is set
(proj1 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) .: ([#] ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj1 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) .: ([#] ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))))) is V11() V12() ext-real Element of REAL
E-bound ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V11() V12() ext-real Element of REAL
upper_bound (proj1 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is V11() V12() ext-real Element of REAL
(proj1 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj1 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) is V11() V12() ext-real Element of REAL
width l is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
c9 `1 is V11() V12() ext-real Element of REAL
E-min ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
E-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is Element of K6( the carrier of (TOP-REAL 2))
SE-corner ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
S-bound ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V11() V12() ext-real Element of REAL
proj2 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V13() V16( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))), REAL ) V197((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) Element of K6(K7( the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))),REAL))
lower_bound (proj2 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is V11() V12() ext-real Element of REAL
(proj2 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) is V11() V12() ext-real Element of REAL
|[(E-bound ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))),(S-bound ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NE-corner ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
N-bound ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is V11() V12() ext-real Element of REAL
upper_bound (proj2 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is V11() V12() ext-real Element of REAL
upper_bound ((proj2 | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) .: the carrier of ((TOP-REAL 2) | ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) is V11() V12() ext-real Element of REAL
|[(E-bound ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))),(N-bound ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SE-corner ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))),(NE-corner ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SE-corner ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))),(NE-corner ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))))) /\ ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (E-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is strict SubSpace of TOP-REAL 2
proj2 | (E-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) is V13() V16( the carrier of ((TOP-REAL 2) | (E-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (E-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))), REAL ) V197((TOP-REAL 2) | (E-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))),REAL))
the carrier of ((TOP-REAL 2) | (E-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) is set
K7( the carrier of ((TOP-REAL 2) | (E-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (E-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))),REAL)) is set
lower_bound (proj2 | (E-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) is V11() V12() ext-real Element of REAL
(proj2 | (E-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) .: the carrier of ((TOP-REAL 2) | (E-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | (E-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))) .: the carrier of ((TOP-REAL 2) | (E-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))))) is V11() V12() ext-real Element of REAL
|[(E-bound ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))),(lower_bound (proj2 | (E-most ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k)))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(E-min ((LSeg ((l * (i,C)),(l * (p,C)))) /\ (L~ k))) `1 is V11() V12() ext-real Element of REAL
len l is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(l * (i,C)) `1 is V11() V12() ext-real Element of REAL
(l * (p,C)) `1 is V11() V12() ext-real Element of REAL
(l * (i,C)) `2 is V11() V12() ext-real Element of REAL
l * (1,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (1,C)) `2 is V11() V12() ext-real Element of REAL
(l * (p,C)) `2 is V11() V12() ext-real Element of REAL
len k is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
{ (LSeg (k,b1)) where b1 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT : ( 1 <= b1 & b1 + 1 <= len k ) } is set
union { (LSeg (k,b1)) where b1 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT : ( 1 <= b1 & b1 + 1 <= len k ) } is set
j2 is set
i1 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
LSeg (k,i1) is Element of K6( the carrier of (TOP-REAL 2))
i1 + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
k /. i1 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
k /. (i1 + 1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((k /. i1),(k /. (i1 + 1))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
Seg (len k) is V138() V139() V140() V141() V142() V143() Element of K6(NAT)
dom k is V138() V139() V140() V141() V142() V143() Element of K6(NAT)
jo is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
io is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[jo,io] is set
{jo,io} is non empty V138() V139() V140() V141() V142() V143() set
{jo} is non empty V138() V139() V140() V141() V142() V143() set
{{jo,io},{jo}} is non empty set
l * (jo,io) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
j0 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
i0 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[j0,i0] is set
{j0,i0} is non empty V138() V139() V140() V141() V142() V143() set
{j0} is non empty V138() V139() V140() V141() V142() V143() set
{{j0,i0},{j0}} is non empty set
l * (j0,i0) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(k /. i1) `2 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `2 is V11() V12() ext-real Element of REAL
l * (i,io) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (i,io)) `2 is V11() V12() ext-real Element of REAL
l * (1,io) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (1,io)) `2 is V11() V12() ext-real Element of REAL
(l * (jo,io)) `2 is V11() V12() ext-real Element of REAL
c9 `2 is V11() V12() ext-real Element of REAL
l * (i,i0) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (i,i0)) `2 is V11() V12() ext-real Element of REAL
l * (1,i0) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (1,i0)) `2 is V11() V12() ext-real Element of REAL
(l * (j0,i0)) `2 is V11() V12() ext-real Element of REAL
(k /. i1) `1 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `1 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (n,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l * (jo,1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (jo,1)) `1 is V11() V12() ext-real Element of REAL
(l * (n,C)) `1 is V11() V12() ext-real Element of REAL
(l * (n,C)) `2 is V11() V12() ext-real Element of REAL
(l * (j0,i0)) `1 is V11() V12() ext-real Element of REAL
l * (j0,1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (j0,1)) `1 is V11() V12() ext-real Element of REAL
l * (j0,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (j0,C)) `1 is V11() V12() ext-real Element of REAL
i0 - io is V11() V12() ext-real set
abs (i0 - io) is V11() V12() ext-real Element of REAL
j0 - jo is V11() V12() ext-real set
abs (j0 - jo) is V11() V12() ext-real Element of REAL
(abs (i0 - io)) + (abs (j0 - jo)) is V11() V12() ext-real set
0 + (abs (j0 - jo)) is V11() V12() ext-real set
- (j0 - jo) is V11() V12() ext-real set
abs (- (j0 - jo)) is V11() V12() ext-real Element of REAL
jo + 0 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
jo - j0 is V11() V12() ext-real set
j0 + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (jo,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (jo,C)) `1 is V11() V12() ext-real Element of REAL
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (n,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (n,C)) `2 is V11() V12() ext-real Element of REAL
(k /. i1) `1 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `1 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (n,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l * (j0,1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (j0,1)) `1 is V11() V12() ext-real Element of REAL
(l * (n,C)) `1 is V11() V12() ext-real Element of REAL
(l * (n,C)) `2 is V11() V12() ext-real Element of REAL
(l * (jo,io)) `1 is V11() V12() ext-real Element of REAL
l * (jo,1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (jo,1)) `1 is V11() V12() ext-real Element of REAL
l * (jo,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (jo,C)) `1 is V11() V12() ext-real Element of REAL
j0 + 0 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
jo - j0 is V11() V12() ext-real set
- 0 is empty V11() V12() Function-like functional ext-real non positive non negative V138() V139() V140() V141() V142() V143() V144() set
- (jo - j0) is V11() V12() ext-real set
i0 - io is V11() V12() ext-real set
abs (i0 - io) is V11() V12() ext-real Element of REAL
j0 - jo is V11() V12() ext-real set
abs (j0 - jo) is V11() V12() ext-real Element of REAL
(abs (i0 - io)) + (abs (j0 - jo)) is V11() V12() ext-real set
0 + (abs (j0 - jo)) is V11() V12() ext-real set
jo + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
j0 - 0 is V11() V12() ext-real non negative set
l * (j0,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (j0,C)) `1 is V11() V12() ext-real Element of REAL
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (n,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (n,C)) `2 is V11() V12() ext-real Element of REAL
(k /. i1) `1 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `1 is V11() V12() ext-real Element of REAL
(k /. i1) `1 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `1 is V11() V12() ext-real Element of REAL
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (n,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l * (j0,1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(l * (j0,1)) `1 is V11() V12() ext-real Element of REAL
(l * (n,C)) `1 is V11() V12() ext-real Element of REAL
c9 `2 is V11() V12() ext-real Element of REAL
(l * (n,C)) `2 is V11() V12() ext-real Element of REAL
(k /. i1) `2 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `2 is V11() V12() ext-real Element of REAL
(k /. i1) `1 is V11() V12() ext-real Element of REAL
(k /. (i1 + 1)) `1 is V11() V12() ext-real Element of REAL
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l * (n,C) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
i is non empty compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
C is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
Upper_Seq (i,C) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2)
(Upper_Seq (i,C)) /. 1 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
Cage (i,C) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded V186() V187() V188() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (i,C)) is non empty connected being_simple_closed_curve compact Element of K6( the carrier of (TOP-REAL 2))
W-min (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
W-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (i,C))) is strict compact SubSpace of TOP-REAL 2
proj1 | (L~ (Cage (i,C))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))), REAL ) V197((TOP-REAL 2) | (L~ (Cage (i,C)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL))
the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is set
K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL)) is set
lower_bound (proj1 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
(proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
W-most (L~ (Cage (i,C))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
SW-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
S-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
proj2 | (L~ (Cage (i,C))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))), REAL ) V197((TOP-REAL 2) | (L~ (Cage (i,C)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL))
lower_bound (proj2 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
(proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (i,C)))),(S-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NW-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
N-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
upper_bound (proj2 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
upper_bound ((proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (i,C)))),(N-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (i,C)))),(NW-corner (L~ (Cage (i,C))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SW-corner (L~ (Cage (i,C)))),(NW-corner (L~ (Cage (i,C)))))) /\ (L~ (Cage (i,C))) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ (Cage (i,C)))) is strict compact SubSpace of TOP-REAL 2
proj2 | (W-most (L~ (Cage (i,C)))) is V13() V16( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C)))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))), REAL ) V197((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL))
the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) is set
K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL)) is set
lower_bound (proj2 | (W-most (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
(proj2 | (W-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | (W-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C)))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (i,C)))),(lower_bound (proj2 | (W-most (L~ (Cage (i,C))))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
E-max (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
E-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
upper_bound (proj1 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
upper_bound ((proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
E-most (L~ (Cage (i,C))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
SE-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
|[(E-bound (L~ (Cage (i,C)))),(S-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NE-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
|[(E-bound (L~ (Cage (i,C)))),(N-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (i,C)))),(NE-corner (L~ (Cage (i,C))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SE-corner (L~ (Cage (i,C)))),(NE-corner (L~ (Cage (i,C)))))) /\ (L~ (Cage (i,C))) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ (Cage (i,C)))) is strict compact SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (i,C)))) is V13() V16( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C)))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))), REAL ) V197((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL))
the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) is set
K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL)) is set
upper_bound (proj2 | (E-most (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
(proj2 | (E-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj2 | (E-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (i,C)))),(upper_bound (proj2 | (E-most (L~ (Cage (i,C))))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
rng (Cage (i,C)) is V2() Element of K6( the carrier of (TOP-REAL 2))
Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C))))) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like circular FinSequence of the carrier of (TOP-REAL 2)
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) -: (E-max (L~ (Cage (i,C)))) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
rng (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) is Element of K6( the carrier of (TOP-REAL 2))
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) /. 1 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
i is non empty compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
C is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
Lower_Seq (i,C) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2)
(Lower_Seq (i,C)) /. 1 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
Cage (i,C) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded V186() V187() V188() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (i,C)) is non empty connected being_simple_closed_curve compact Element of K6( the carrier of (TOP-REAL 2))
E-max (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
E-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (i,C))) is strict compact SubSpace of TOP-REAL 2
proj1 | (L~ (Cage (i,C))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))), REAL ) V197((TOP-REAL 2) | (L~ (Cage (i,C)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL))
the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is set
K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL)) is set
upper_bound (proj1 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
(proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
E-most (L~ (Cage (i,C))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
SE-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
S-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
proj2 | (L~ (Cage (i,C))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))), REAL ) V197((TOP-REAL 2) | (L~ (Cage (i,C)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL))
lower_bound (proj2 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
(proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (i,C)))),(S-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NE-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
N-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
upper_bound (proj2 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
upper_bound ((proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (i,C)))),(N-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (i,C)))),(NE-corner (L~ (Cage (i,C))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SE-corner (L~ (Cage (i,C)))),(NE-corner (L~ (Cage (i,C)))))) /\ (L~ (Cage (i,C))) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ (Cage (i,C)))) is strict compact SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (i,C)))) is V13() V16( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C)))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))), REAL ) V197((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL))
the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) is set
K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL)) is set
upper_bound (proj2 | (E-most (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
(proj2 | (E-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj2 | (E-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (i,C)))),(upper_bound (proj2 | (E-most (L~ (Cage (i,C))))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
W-min (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
W-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
lower_bound (proj1 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
lower_bound ((proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
W-most (L~ (Cage (i,C))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
SW-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
|[(W-bound (L~ (Cage (i,C)))),(S-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NW-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
|[(W-bound (L~ (Cage (i,C)))),(N-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (i,C)))),(NW-corner (L~ (Cage (i,C))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SW-corner (L~ (Cage (i,C)))),(NW-corner (L~ (Cage (i,C)))))) /\ (L~ (Cage (i,C))) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ (Cage (i,C)))) is strict compact SubSpace of TOP-REAL 2
proj2 | (W-most (L~ (Cage (i,C)))) is V13() V16( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C)))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))), REAL ) V197((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL))
the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) is set
K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL)) is set
lower_bound (proj2 | (W-most (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
(proj2 | (W-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | (W-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C)))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (i,C)))),(lower_bound (proj2 | (W-most (L~ (Cage (i,C))))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C))))) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like circular FinSequence of the carrier of (TOP-REAL 2)
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) :- (E-max (L~ (Cage (i,C)))) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
i is non empty compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
C is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
Upper_Seq (i,C) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2)
len (Upper_Seq (i,C)) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(Upper_Seq (i,C)) /. (len (Upper_Seq (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
Cage (i,C) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded V186() V187() V188() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (i,C)) is non empty connected being_simple_closed_curve compact Element of K6( the carrier of (TOP-REAL 2))
E-max (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
E-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (i,C))) is strict compact SubSpace of TOP-REAL 2
proj1 | (L~ (Cage (i,C))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))), REAL ) V197((TOP-REAL 2) | (L~ (Cage (i,C)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL))
the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is set
K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL)) is set
upper_bound (proj1 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
(proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
E-most (L~ (Cage (i,C))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
SE-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
S-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
proj2 | (L~ (Cage (i,C))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))), REAL ) V197((TOP-REAL 2) | (L~ (Cage (i,C)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL))
lower_bound (proj2 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
(proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (i,C)))),(S-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NE-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
N-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
upper_bound (proj2 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
upper_bound ((proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (i,C)))),(N-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (i,C)))),(NE-corner (L~ (Cage (i,C))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SE-corner (L~ (Cage (i,C)))),(NE-corner (L~ (Cage (i,C)))))) /\ (L~ (Cage (i,C))) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ (Cage (i,C)))) is strict compact SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (i,C)))) is V13() V16( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C)))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))), REAL ) V197((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL))
the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) is set
K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL)) is set
upper_bound (proj2 | (E-most (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
(proj2 | (E-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj2 | (E-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (i,C)))),(upper_bound (proj2 | (E-most (L~ (Cage (i,C))))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
W-min (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
W-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
lower_bound (proj1 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
lower_bound ((proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
W-most (L~ (Cage (i,C))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
SW-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
|[(W-bound (L~ (Cage (i,C)))),(S-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NW-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
|[(W-bound (L~ (Cage (i,C)))),(N-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (i,C)))),(NW-corner (L~ (Cage (i,C))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SW-corner (L~ (Cage (i,C)))),(NW-corner (L~ (Cage (i,C)))))) /\ (L~ (Cage (i,C))) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ (Cage (i,C)))) is strict compact SubSpace of TOP-REAL 2
proj2 | (W-most (L~ (Cage (i,C)))) is V13() V16( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C)))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))), REAL ) V197((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL))
the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) is set
K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL)) is set
lower_bound (proj2 | (W-most (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
(proj2 | (W-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | (W-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C)))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (i,C)))),(lower_bound (proj2 | (W-most (L~ (Cage (i,C))))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C))))) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like circular FinSequence of the carrier of (TOP-REAL 2)
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) -: (E-max (L~ (Cage (i,C)))) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
rng (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) is Element of K6( the carrier of (TOP-REAL 2))
rng (Cage (i,C)) is V2() Element of K6( the carrier of (TOP-REAL 2))
(E-max (L~ (Cage (i,C)))) .. (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
i is non empty compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
C is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
Lower_Seq (i,C) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2)
len (Lower_Seq (i,C)) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(Lower_Seq (i,C)) /. (len (Lower_Seq (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
Cage (i,C) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded V186() V187() V188() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (i,C)) is non empty connected being_simple_closed_curve compact Element of K6( the carrier of (TOP-REAL 2))
W-min (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
W-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (i,C))) is strict compact SubSpace of TOP-REAL 2
proj1 | (L~ (Cage (i,C))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))), REAL ) V197((TOP-REAL 2) | (L~ (Cage (i,C)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL))
the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is set
K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL)) is set
lower_bound (proj1 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
(proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
W-most (L~ (Cage (i,C))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
SW-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
S-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
proj2 | (L~ (Cage (i,C))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))), REAL ) V197((TOP-REAL 2) | (L~ (Cage (i,C)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL))
lower_bound (proj2 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
(proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (i,C)))),(S-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NW-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
N-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
upper_bound (proj2 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
upper_bound ((proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (i,C)))),(N-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (i,C)))),(NW-corner (L~ (Cage (i,C))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SW-corner (L~ (Cage (i,C)))),(NW-corner (L~ (Cage (i,C)))))) /\ (L~ (Cage (i,C))) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ (Cage (i,C)))) is strict compact SubSpace of TOP-REAL 2
proj2 | (W-most (L~ (Cage (i,C)))) is V13() V16( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C)))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))), REAL ) V197((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL))
the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) is set
K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL)) is set
lower_bound (proj2 | (W-most (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
(proj2 | (W-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | (W-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C)))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (i,C)))),(lower_bound (proj2 | (W-most (L~ (Cage (i,C))))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
rng (Cage (i,C)) is V2() Element of K6( the carrier of (TOP-REAL 2))
E-max (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
E-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
upper_bound (proj1 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
upper_bound ((proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
E-most (L~ (Cage (i,C))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
SE-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
|[(E-bound (L~ (Cage (i,C)))),(S-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NE-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
|[(E-bound (L~ (Cage (i,C)))),(N-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (i,C)))),(NE-corner (L~ (Cage (i,C))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SE-corner (L~ (Cage (i,C)))),(NE-corner (L~ (Cage (i,C)))))) /\ (L~ (Cage (i,C))) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ (Cage (i,C)))) is strict compact SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (i,C)))) is V13() V16( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C)))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))), REAL ) V197((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL))
the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) is set
K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL)) is set
upper_bound (proj2 | (E-most (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
(proj2 | (E-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj2 | (E-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (i,C)))),(upper_bound (proj2 | (E-most (L~ (Cage (i,C))))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C))))) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like circular FinSequence of the carrier of (TOP-REAL 2)
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) :- (E-max (L~ (Cage (i,C)))) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
rng (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) is Element of K6( the carrier of (TOP-REAL 2))
len (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) /. (len (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C))))))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) /. 1 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
i is non empty compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
C is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
Upper_Seq (i,C) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2)
L~ (Upper_Seq (i,C)) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
Cage (i,C) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded V186() V187() V188() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (i,C)) is non empty connected being_simple_closed_curve compact Element of K6( the carrier of (TOP-REAL 2))
Upper_Arc (L~ (Cage (i,C))) is non empty Element of K6( the carrier of (TOP-REAL 2))
Lower_Seq (i,C) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2)
L~ (Lower_Seq (i,C)) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
Lower_Arc (L~ (Cage (i,C))) is non empty Element of K6( the carrier of (TOP-REAL 2))
W-min (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
W-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (i,C))) is strict compact SubSpace of TOP-REAL 2
proj1 | (L~ (Cage (i,C))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))), REAL ) V197((TOP-REAL 2) | (L~ (Cage (i,C)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL))
the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is set
K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL)) is set
lower_bound (proj1 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
(proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
W-most (L~ (Cage (i,C))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
SW-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
S-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
proj2 | (L~ (Cage (i,C))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))), REAL ) V197((TOP-REAL 2) | (L~ (Cage (i,C)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL))
lower_bound (proj2 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
(proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (i,C)))),(S-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NW-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
N-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
upper_bound (proj2 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
upper_bound ((proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (i,C)))),(N-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (i,C)))),(NW-corner (L~ (Cage (i,C))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SW-corner (L~ (Cage (i,C)))),(NW-corner (L~ (Cage (i,C)))))) /\ (L~ (Cage (i,C))) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ (Cage (i,C)))) is strict compact SubSpace of TOP-REAL 2
proj2 | (W-most (L~ (Cage (i,C)))) is V13() V16( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C)))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))), REAL ) V197((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL))
the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) is set
K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL)) is set
lower_bound (proj2 | (W-most (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
(proj2 | (W-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | (W-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C)))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (i,C)))),(lower_bound (proj2 | (W-most (L~ (Cage (i,C))))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
E-max (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
E-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
upper_bound (proj1 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
upper_bound ((proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
E-most (L~ (Cage (i,C))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
SE-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
|[(E-bound (L~ (Cage (i,C)))),(S-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NE-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
|[(E-bound (L~ (Cage (i,C)))),(N-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (i,C)))),(NE-corner (L~ (Cage (i,C))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SE-corner (L~ (Cage (i,C)))),(NE-corner (L~ (Cage (i,C)))))) /\ (L~ (Cage (i,C))) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ (Cage (i,C)))) is strict compact SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (i,C)))) is V13() V16( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C)))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))), REAL ) V197((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL))
the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) is set
K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL)) is set
upper_bound (proj2 | (E-most (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
(proj2 | (E-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj2 | (E-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (i,C)))),(upper_bound (proj2 | (E-most (L~ (Cage (i,C))))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(Upper_Arc (L~ (Cage (i,C)))) \/ (Lower_Arc (L~ (Cage (i,C)))) is non empty Element of K6( the carrier of (TOP-REAL 2))
(Upper_Seq (i,C)) /. 1 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
len (Upper_Seq (i,C)) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(Upper_Seq (i,C)) /. (len (Upper_Seq (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(Lower_Seq (i,C)) /. 1 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
len (Lower_Seq (i,C)) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(Lower_Seq (i,C)) /. (len (Lower_Seq (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(L~ (Upper_Seq (i,C))) \/ (L~ (Lower_Seq (i,C))) is non empty Element of K6( the carrier of (TOP-REAL 2))
i is non empty connected compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
C is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
Upper_Seq (i,C) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2)
Gauge (i,C) is V13() non empty-yielding V16( NAT ) V17(K337( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K337( the carrier of (TOP-REAL 2))
Cage (i,C) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded V186() V187() V188() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (i,C)) is non empty connected being_simple_closed_curve compact Element of K6( the carrier of (TOP-REAL 2))
W-min (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
W-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (i,C))) is strict compact SubSpace of TOP-REAL 2
proj1 | (L~ (Cage (i,C))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))), REAL ) V197((TOP-REAL 2) | (L~ (Cage (i,C)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL))
the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is set
K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL)) is set
lower_bound (proj1 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
(proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
W-most (L~ (Cage (i,C))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
SW-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
S-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
proj2 | (L~ (Cage (i,C))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))), REAL ) V197((TOP-REAL 2) | (L~ (Cage (i,C)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL))
lower_bound (proj2 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
(proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (i,C)))),(S-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NW-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
N-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
upper_bound (proj2 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
upper_bound ((proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (i,C)))),(N-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (i,C)))),(NW-corner (L~ (Cage (i,C))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SW-corner (L~ (Cage (i,C)))),(NW-corner (L~ (Cage (i,C)))))) /\ (L~ (Cage (i,C))) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ (Cage (i,C)))) is strict compact SubSpace of TOP-REAL 2
proj2 | (W-most (L~ (Cage (i,C)))) is V13() V16( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C)))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))), REAL ) V197((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL))
the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) is set
K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL)) is set
lower_bound (proj2 | (W-most (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
(proj2 | (W-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | (W-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C)))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (i,C)))),(lower_bound (proj2 | (W-most (L~ (Cage (i,C))))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C))))) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like circular FinSequence of the carrier of (TOP-REAL 2)
E-max (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
E-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
upper_bound (proj1 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
upper_bound ((proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
E-most (L~ (Cage (i,C))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
SE-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
|[(E-bound (L~ (Cage (i,C)))),(S-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NE-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
|[(E-bound (L~ (Cage (i,C)))),(N-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (i,C)))),(NE-corner (L~ (Cage (i,C))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SE-corner (L~ (Cage (i,C)))),(NE-corner (L~ (Cage (i,C)))))) /\ (L~ (Cage (i,C))) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ (Cage (i,C)))) is strict compact SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (i,C)))) is V13() V16( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C)))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))), REAL ) V197((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL))
the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) is set
K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL)) is set
upper_bound (proj2 | (E-most (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
(proj2 | (E-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj2 | (E-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (i,C)))),(upper_bound (proj2 | (E-most (L~ (Cage (i,C))))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) -: (E-max (L~ (Cage (i,C)))) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
(E-max (L~ (Cage (i,C)))) .. (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) | ((E-max (L~ (Cage (i,C)))) .. (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C))))))) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
i is V13() non empty-yielding V16( NAT ) V17(K337( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K337( the carrier of (TOP-REAL 2))
Indices i is set
C is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
<*C*> is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like special FinSequence of the carrier of (TOP-REAL 2)
p is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
p /. 1 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
<*C*> ^ p is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
k is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[k,l] is set
{k,l} is non empty V138() V139() V140() V141() V142() V143() set
{k} is non empty V138() V139() V140() V141() V142() V143() set
{{k,l},{k}} is non empty set
G is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
f is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[G,f] is set
{G,f} is non empty V138() V139() V140() V141() V142() V143() set
{G} is non empty V138() V139() V140() V141() V142() V143() set
{{G,f},{G}} is non empty set
len <*C*> is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
<*C*> /. (len <*C*>) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
i * (k,l) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
i * (G,f) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
dom <*C*> is V138() V139() V140() V141() V142() V143() Element of K6(NAT)
dom p is V138() V139() V140() V141() V142() V143() Element of K6(NAT)
<*C*> . (len <*C*>) is set
G - k is V11() V12() ext-real set
abs (G - k) is V11() V12() ext-real Element of REAL
f - l is V11() V12() ext-real set
abs (f - l) is V11() V12() ext-real Element of REAL
(abs (G - k)) + (abs (f - l)) is V11() V12() ext-real set
k - G is V11() V12() ext-real set
abs (k - G) is V11() V12() ext-real Element of REAL
(abs (k - G)) + (abs (f - l)) is V11() V12() ext-real set
l - f is V11() V12() ext-real set
abs (l - f) is V11() V12() ext-real Element of REAL
(abs (k - G)) + (abs (l - f)) is V11() V12() ext-real set
k is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
dom (<*C*> ^ p) is V138() V139() V140() V141() V142() V143() Element of K6(NAT)
l is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
G is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[l,G] is set
{l,G} is non empty V138() V139() V140() V141() V142() V143() set
{l} is non empty V138() V139() V140() V141() V142() V143() set
{{l,G},{l}} is non empty set
i * (l,G) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
G is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[l,G] is set
{l,G} is non empty V138() V139() V140() V141() V142() V143() set
{l} is non empty V138() V139() V140() V141() V142() V143() set
{{l,G},{l}} is non empty set
i * (l,G) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
f is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[f,n] is set
{f,n} is non empty V138() V139() V140() V141() V142() V143() set
{f} is non empty V138() V139() V140() V141() V142() V143() set
{{f,n},{f}} is non empty set
<*C*> . k is set
<*C*> /. k is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(<*C*> ^ p) /. k is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
i * (f,n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l is V6() V10() V11() V12() ext-real non negative set
(len <*C*>) + l is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l is V6() V10() V11() V12() ext-real non negative set
(len <*C*>) + l is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
p /. l is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
G is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
f is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[G,f] is set
{G,f} is non empty V138() V139() V140() V141() V142() V143() set
{G} is non empty V138() V139() V140() V141() V142() V143() set
{{G,f},{G}} is non empty set
i * (G,f) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
c9 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[n,c9] is set
{n,c9} is non empty V138() V139() V140() V141() V142() V143() set
{n} is non empty V138() V139() V140() V141() V142() V143() set
{{n,c9},{n}} is non empty set
(<*C*> ^ p) /. k is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
i * (n,c9) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
k is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
k + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
1 + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
<*C*> /. k is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
<*C*> /. (k + 1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
G is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[l,G] is set
{l,G} is non empty V138() V139() V140() V141() V142() V143() set
{l} is non empty V138() V139() V140() V141() V142() V143() set
{{l,G},{l}} is non empty set
f is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[f,n] is set
{f,n} is non empty V138() V139() V140() V141() V142() V143() set
{f} is non empty V138() V139() V140() V141() V142() V143() set
{{f,n},{f}} is non empty set
i * (l,G) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
i * (f,n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l - f is V11() V12() ext-real set
abs (l - f) is V11() V12() ext-real Element of REAL
G - n is V11() V12() ext-real set
abs (G - n) is V11() V12() ext-real Element of REAL
(abs (l - f)) + (abs (G - n)) is V11() V12() ext-real set
k is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
k + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
G is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[l,G] is set
{l,G} is non empty V138() V139() V140() V141() V142() V143() set
{l} is non empty V138() V139() V140() V141() V142() V143() set
{{l,G},{l}} is non empty set
f is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[f,n] is set
{f,n} is non empty V138() V139() V140() V141() V142() V143() set
{f} is non empty V138() V139() V140() V141() V142() V143() set
{{f,n},{f}} is non empty set
p /. k is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
i * (l,G) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
p /. (k + 1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
i * (f,n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l - f is V11() V12() ext-real set
abs (l - f) is V11() V12() ext-real Element of REAL
G - n is V11() V12() ext-real set
abs (G - n) is V11() V12() ext-real Element of REAL
(abs (l - f)) + (abs (G - n)) is V11() V12() ext-real set
k is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
k + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
l is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
G is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[l,G] is set
{l,G} is non empty V138() V139() V140() V141() V142() V143() set
{l} is non empty V138() V139() V140() V141() V142() V143() set
{{l,G},{l}} is non empty set
f is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[f,n] is set
{f,n} is non empty V138() V139() V140() V141() V142() V143() set
{f} is non empty V138() V139() V140() V141() V142() V143() set
{{f,n},{f}} is non empty set
(<*C*> ^ p) /. k is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
i * (l,G) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(<*C*> ^ p) /. (k + 1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
i * (f,n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
l - f is V11() V12() ext-real set
abs (l - f) is V11() V12() ext-real Element of REAL
G - n is V11() V12() ext-real set
abs (G - n) is V11() V12() ext-real Element of REAL
(abs (l - f)) + (abs (G - n)) is V11() V12() ext-real set
i is non empty connected compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
C is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
Lower_Seq (i,C) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2)
Gauge (i,C) is V13() non empty-yielding V16( NAT ) V17(K337( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K337( the carrier of (TOP-REAL 2))
width (Gauge (i,C)) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
Cage (i,C) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded V186() V187() V188() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (i,C)) is non empty connected being_simple_closed_curve compact Element of K6( the carrier of (TOP-REAL 2))
E-max (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
E-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (i,C))) is strict compact SubSpace of TOP-REAL 2
proj1 | (L~ (Cage (i,C))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))), REAL ) V197((TOP-REAL 2) | (L~ (Cage (i,C)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL))
the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is set
K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL)) is set
upper_bound (proj1 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
(proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
E-most (L~ (Cage (i,C))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
SE-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
S-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
proj2 | (L~ (Cage (i,C))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))), REAL ) V197((TOP-REAL 2) | (L~ (Cage (i,C)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))),REAL))
lower_bound (proj2 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
(proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C)))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (i,C)))),(S-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NE-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
N-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
upper_bound (proj2 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
upper_bound ((proj2 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (i,C)))),(N-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (i,C)))),(NE-corner (L~ (Cage (i,C))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SE-corner (L~ (Cage (i,C)))),(NE-corner (L~ (Cage (i,C)))))) /\ (L~ (Cage (i,C))) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ (Cage (i,C)))) is strict compact SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (i,C)))) is V13() V16( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C)))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))), REAL ) V197((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL))
the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) is set
K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))),REAL)) is set
upper_bound (proj2 | (E-most (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
(proj2 | (E-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C))))) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj2 | (E-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (i,C)))),(upper_bound (proj2 | (E-most (L~ (Cage (i,C))))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
len (Gauge (i,C)) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
p is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(Gauge (i,C)) * ((len (Gauge (i,C))),p) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
W-min (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
W-bound (L~ (Cage (i,C))) is V11() V12() ext-real Element of REAL
lower_bound (proj1 | (L~ (Cage (i,C)))) is V11() V12() ext-real Element of REAL
lower_bound ((proj1 | (L~ (Cage (i,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
W-most (L~ (Cage (i,C))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
SW-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
|[(W-bound (L~ (Cage (i,C)))),(S-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
NW-corner (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
|[(W-bound (L~ (Cage (i,C)))),(N-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (i,C)))),(NW-corner (L~ (Cage (i,C))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SW-corner (L~ (Cage (i,C)))),(NW-corner (L~ (Cage (i,C)))))) /\ (L~ (Cage (i,C))) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ (Cage (i,C)))) is strict compact SubSpace of TOP-REAL 2
proj2 | (W-most (L~ (Cage (i,C)))) is V13() V16( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C)))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))), REAL ) V197((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL))
the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) is set
K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))),REAL)) is set
lower_bound (proj2 | (W-most (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
(proj2 | (W-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C))))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj2 | (W-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (i,C)))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (i,C)))),(lower_bound (proj2 | (W-most (L~ (Cage (i,C))))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C))))) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like circular FinSequence of the carrier of (TOP-REAL 2)
(E-max (L~ (Cage (i,C)))) .. (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) /^ ((E-max (L~ (Cage (i,C)))) .. (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C))))))) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
((Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) /^ ((E-max (L~ (Cage (i,C)))) .. (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))))) /. 1 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) :- (E-max (L~ (Cage (i,C)))) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
<*(E-max (L~ (Cage (i,C))))*> is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like special FinSequence of the carrier of (TOP-REAL 2)
<*(E-max (L~ (Cage (i,C))))*> ^ ((Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) /^ ((E-max (L~ (Cage (i,C)))) .. (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))))) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
Indices (Gauge (i,C)) is set
(E-max (L~ (Cage (i,C)))) .. (Cage (i,C)) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
f is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[f,n] is set
{f,n} is non empty V138() V139() V140() V141() V142() V143() set
{f} is non empty V138() V139() V140() V141() V142() V143() set
{{f,n},{f}} is non empty set
(Gauge (i,C)) * (f,n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
c9 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
c9 - f is V11() V12() ext-real set
abs (c9 - f) is V11() V12() ext-real Element of REAL
j2 is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[c9,j2] is set
{c9,j2} is non empty V138() V139() V140() V141() V142() V143() set
{c9} is non empty V138() V139() V140() V141() V142() V143() set
{{c9,j2},{c9}} is non empty set
(Gauge (i,C)) * (c9,j2) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
j2 - n is V11() V12() ext-real set
abs (j2 - n) is V11() V12() ext-real Element of REAL
(abs (c9 - f)) + (abs (j2 - n)) is V11() V12() ext-real set
len (Cage (i,C)) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
dom (Cage (i,C)) is V2() V138() V139() V140() V141() V142() V143() Element of K6(NAT)
rng (Cage (i,C)) is V2() Element of K6( the carrier of (TOP-REAL 2))
(Cage (i,C)) /. 1 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
N-min (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
N-most (L~ (Cage (i,C))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
LSeg ((NW-corner (L~ (Cage (i,C)))),(NE-corner (L~ (Cage (i,C))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((NW-corner (L~ (Cage (i,C)))),(NE-corner (L~ (Cage (i,C)))))) /\ (L~ (Cage (i,C))) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (N-most (L~ (Cage (i,C)))) is strict compact SubSpace of TOP-REAL 2
proj1 | (N-most (L~ (Cage (i,C)))) is V13() V16( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (i,C)))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (i,C))))), REAL ) V197((TOP-REAL 2) | (N-most (L~ (Cage (i,C))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (i,C))))),REAL))
the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (i,C))))) is set
K7( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (i,C))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (i,C))))),REAL)) is set
lower_bound (proj1 | (N-most (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
(proj1 | (N-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (i,C))))) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj1 | (N-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (i,C)))))) is V11() V12() ext-real Element of REAL
|[(lower_bound (proj1 | (N-most (L~ (Cage (i,C)))))),(N-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
E-min (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
lower_bound (proj2 | (E-most (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
lower_bound ((proj2 | (E-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (i,C)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (i,C)))),(lower_bound (proj2 | (E-most (L~ (Cage (i,C))))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(E-min (L~ (Cage (i,C)))) .. (Cage (i,C)) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
S-max (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
S-most (L~ (Cage (i,C))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
LSeg ((SW-corner (L~ (Cage (i,C)))),(SE-corner (L~ (Cage (i,C))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SW-corner (L~ (Cage (i,C)))),(SE-corner (L~ (Cage (i,C)))))) /\ (L~ (Cage (i,C))) is compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (S-most (L~ (Cage (i,C)))) is strict compact SubSpace of TOP-REAL 2
proj1 | (S-most (L~ (Cage (i,C)))) is V13() V16( the carrier of ((TOP-REAL 2) | (S-most (L~ (Cage (i,C)))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (S-most (L~ (Cage (i,C))))), REAL ) V197((TOP-REAL 2) | (S-most (L~ (Cage (i,C))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (S-most (L~ (Cage (i,C))))),REAL))
the carrier of ((TOP-REAL 2) | (S-most (L~ (Cage (i,C))))) is set
K7( the carrier of ((TOP-REAL 2) | (S-most (L~ (Cage (i,C))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (S-most (L~ (Cage (i,C))))),REAL)) is set
upper_bound (proj1 | (S-most (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
(proj1 | (S-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ (Cage (i,C))))) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj1 | (S-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ (Cage (i,C)))))) is V11() V12() ext-real Element of REAL
|[(upper_bound (proj1 | (S-most (L~ (Cage (i,C)))))),(S-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(S-max (L~ (Cage (i,C)))) .. (Cage (i,C)) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
S-min (L~ (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
lower_bound (proj1 | (S-most (L~ (Cage (i,C))))) is V11() V12() ext-real Element of REAL
lower_bound ((proj1 | (S-most (L~ (Cage (i,C))))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ (Cage (i,C)))))) is V11() V12() ext-real Element of REAL
|[(lower_bound (proj1 | (S-most (L~ (Cage (i,C)))))),(S-bound (L~ (Cage (i,C))))]| is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(S-min (L~ (Cage (i,C)))) .. (Cage (i,C)) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(W-min (L~ (Cage (i,C)))) .. (Cage (i,C)) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(len (Cage (i,C))) - ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C))) is V11() V12() ext-real set
0 + 0 is empty V6() V10() V11() V12() Function-like functional V37() ext-real non positive non negative V76() V138() V139() V140() V141() V142() V143() V144() Element of NAT
(((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) + 1) + ((len (Cage (i,C))) - ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C)))) is V11() V12() ext-real set
rng (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) is Element of K6( the carrier of (TOP-REAL 2))
len (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
Upper_Seq (i,C) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2)
len (Upper_Seq (i,C)) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
len (Lower_Seq (i,C)) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(len (Cage (i,C))) + (len (Lower_Seq (i,C))) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(len (Cage (i,C))) + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
((E-max (L~ (Cage (i,C)))) .. (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C))))))) + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
1 + ((E-max (L~ (Cage (i,C)))) .. (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C))))))) is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(1 + ((E-max (L~ (Cage (i,C)))) .. (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))))) - ((E-max (L~ (Cage (i,C)))) .. (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C))))))) is V11() V12() ext-real set
(len (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C))))))) - ((E-max (L~ (Cage (i,C)))) .. (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C))))))) is V11() V12() ext-real set
len ((Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) /^ ((E-max (L~ (Cage (i,C)))) .. (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))))) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
dom ((Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) /^ ((E-max (L~ (Cage (i,C)))) .. (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))))) is V138() V139() V140() V141() V142() V143() Element of K6(NAT)
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) /. (((E-max (L~ (Cage (i,C)))) .. (Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C))))))) + 1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(len (Cage (i,C))) + ((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
((len (Cage (i,C))) + ((E-max (L~ (Cage (i,C)))) .. (Cage (i,C)))) - ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C))) is V11() V12() ext-real set
(((len (Cage (i,C))) + ((E-max (L~ (Cage (i,C)))) .. (Cage (i,C)))) - ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C)))) + 1 is V11() V12() ext-real set
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) /. ((((len (Cage (i,C))) + ((E-max (L~ (Cage (i,C)))) .. (Cage (i,C)))) - ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C)))) + 1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) + ((len (Cage (i,C))) - ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C)))) is V11() V12() ext-real set
(((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) + ((len (Cage (i,C))) - ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C))))) + 1 is V11() V12() ext-real set
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) /. ((((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) + ((len (Cage (i,C))) - ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C))))) + 1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(len (Cage (i,C))) -' ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C))) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) + ((len (Cage (i,C))) -' ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C)))) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) + ((len (Cage (i,C))) -' ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C))))) + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) /. ((((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) + ((len (Cage (i,C))) -' ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C))))) + 1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) + 1) + ((len (Cage (i,C))) -' ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C)))) is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) /. ((((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) + 1) + ((len (Cage (i,C))) -' ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C))))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) /. ((((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) + 1) + ((len (Cage (i,C))) - ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C))))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) + 1) + (len (Cage (i,C))) is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
((((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) + 1) + (len (Cage (i,C)))) - ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C))) is V11() V12() ext-real set
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) /. (((((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) + 1) + (len (Cage (i,C)))) - ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C)))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
((((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) + 1) + (len (Cage (i,C)))) -' ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C))) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(Rotate ((Cage (i,C)),(W-min (L~ (Cage (i,C)))))) /. (((((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) + 1) + (len (Cage (i,C)))) -' ((W-min (L~ (Cage (i,C)))) .. (Cage (i,C)))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(Cage (i,C)) /. (((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) + 1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(Cage (i,C)) /. ((E-max (L~ (Cage (i,C)))) .. (Cage (i,C))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
f - c9 is V11() V12() ext-real set
abs (f - c9) is V11() V12() ext-real Element of REAL
n - j2 is V11() V12() ext-real set
abs (n - j2) is V11() V12() ext-real Element of REAL
(abs (f - c9)) + (abs (n - j2)) is V11() V12() ext-real set
(abs (f - c9)) + (abs (j2 - n)) is V11() V12() ext-real set
[(len (Gauge (i,C))),p] is set
{(len (Gauge (i,C))),p} is non empty V138() V139() V140() V141() V142() V143() set
{(len (Gauge (i,C)))} is non empty V138() V139() V140() V141() V142() V143() set
{{(len (Gauge (i,C))),p},{(len (Gauge (i,C)))}} is non empty set
i is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
i + 1 is non empty V6() V10() V11() V12() V37() ext-real positive non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
C is non empty connected being_simple_closed_curve compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
W-bound C is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | C is strict compact SubSpace of TOP-REAL 2
proj1 | C is V13() V16( the carrier of ((TOP-REAL 2) | C)) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | C), REAL ) V197((TOP-REAL 2) | C) Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))
the carrier of ((TOP-REAL 2) | C) is set
K7( the carrier of ((TOP-REAL 2) | C),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | C),REAL)) is set
lower_bound (proj1 | C) is V11() V12() ext-real Element of REAL
(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is V138() V139() V140() Element of K6(REAL)
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() V12() ext-real Element of REAL
E-bound C is V11() V12() ext-real Element of REAL
upper_bound (proj1 | C) is V11() V12() ext-real Element of REAL
upper_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() V12() ext-real Element of REAL
(W-bound C) + (E-bound C) is V11() V12() ext-real set
((W-bound C) + (E-bound C)) / 2 is V11() V12() ext-real Element of COMPLEX
Gauge (C,1) is V13() non empty-yielding V16( NAT ) V17(K337( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K337( the carrier of (TOP-REAL 2))
Center (Gauge (C,1)) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(Gauge (C,1)) * ((Center (Gauge (C,1))),1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
width (Gauge (C,1)) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1)))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1)))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
Cage (C,(i + 1)) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded V186() V187() V188() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,(i + 1))) is non empty connected being_simple_closed_curve compact Element of K6( the carrier of (TOP-REAL 2))
Upper_Arc (L~ (Cage (C,(i + 1)))) is non empty Element of K6( the carrier of (TOP-REAL 2))
(LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1)))))) is V138() V139() V140() Element of K6(REAL)
lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) is V11() V12() ext-real Element of REAL
Gauge (C,(i + 1)) is V13() non empty-yielding V16( NAT ) V17(K337( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K337( the carrier of (TOP-REAL 2))
width (Gauge (C,(i + 1))) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
Center (Gauge (C,(i + 1))) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
p is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
p `1 is V11() V12() ext-real Element of REAL
p `2 is V11() V12() ext-real Element of REAL
Upper_Seq (C,(i + 1)) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2)
L~ (Upper_Seq (C,(i + 1))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
Lower_Seq (C,(i + 1)) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2)
L~ (Lower_Seq (C,(i + 1))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
Lower_Arc (L~ (Cage (C,(i + 1)))) is non empty Element of K6( the carrier of (TOP-REAL 2))
len (Gauge (C,(i + 1))) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[(Center (Gauge (C,(i + 1)))),1] is set
{(Center (Gauge (C,(i + 1)))),1} is non empty V138() V139() V140() V141() V142() V143() set
{(Center (Gauge (C,(i + 1))))} is non empty V138() V139() V140() V141() V142() V143() set
{{(Center (Gauge (C,(i + 1)))),1},{(Center (Gauge (C,(i + 1))))}} is non empty set
Indices (Gauge (C,(i + 1))) is set
[(Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))] is set
{(Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))} is non empty V138() V139() V140() V141() V142() V143() set
{{(Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))},{(Center (Gauge (C,(i + 1))))}} is non empty set
len (Gauge (C,1)) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) is compact Element of K6( the carrier of (TOP-REAL 2))
(Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) is compact Element of K6( the carrier of (TOP-REAL 2))
n is set
c9 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
c9 `2 is V11() V12() ext-real Element of REAL
N-bound (L~ (Cage (C,(i + 1)))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (C,(i + 1)))) is strict compact SubSpace of TOP-REAL 2
proj2 | (L~ (Cage (C,(i + 1)))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,(i + 1)))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,(i + 1))))), REAL ) V197((TOP-REAL 2) | (L~ (Cage (C,(i + 1))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,(i + 1))))),REAL))
the carrier of ((TOP-REAL 2) | (L~ (Cage (C,(i + 1))))) is set
K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,(i + 1))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,(i + 1))))),REAL)) is set
upper_bound (proj2 | (L~ (Cage (C,(i + 1))))) is V11() V12() ext-real Element of REAL
(proj2 | (L~ (Cage (C,(i + 1))))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (C,(i + 1))))) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj2 | (L~ (Cage (C,(i + 1))))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (C,(i + 1)))))) is V11() V12() ext-real Element of REAL
((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))) `2 is V11() V12() ext-real Element of REAL
S-bound (L~ (Cage (C,(i + 1)))) is V11() V12() ext-real Element of REAL
lower_bound (proj2 | (L~ (Cage (C,(i + 1))))) is V11() V12() ext-real Element of REAL
lower_bound ((proj2 | (L~ (Cage (C,(i + 1))))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (C,(i + 1)))))) is V11() V12() ext-real Element of REAL
((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)) `2 is V11() V12() ext-real Element of REAL
((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 is V11() V12() ext-real Element of REAL
((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))) `1 is V11() V12() ext-real Element of REAL
c9 `1 is V11() V12() ext-real Element of REAL
((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)) `1 is V11() V12() ext-real Element of REAL
((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))) `1 is V11() V12() ext-real Element of REAL
proj2 .: ((LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Upper_Seq (C,(i + 1))))) is V138() V139() V140() Element of K6(REAL)
lower_bound (proj2 .: ((LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Upper_Seq (C,(i + 1)))))) is V11() V12() ext-real Element of REAL
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n)) `2 is V11() V12() ext-real Element of REAL
((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 is V11() V12() ext-real Element of REAL
((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n)) `1 is V11() V12() ext-real Element of REAL
Upper_Seq (C,(i + 1)) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2)
L~ (Upper_Seq (C,(i + 1))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
Lower_Arc (L~ (Cage (C,(i + 1)))) is non empty Element of K6( the carrier of (TOP-REAL 2))
Lower_Seq (C,(i + 1)) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2)
L~ (Lower_Seq (C,(i + 1))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
len (Gauge (C,(i + 1))) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
[(Center (Gauge (C,(i + 1)))),1] is set
{(Center (Gauge (C,(i + 1)))),1} is non empty V138() V139() V140() V141() V142() V143() set
{(Center (Gauge (C,(i + 1))))} is non empty V138() V139() V140() V141() V142() V143() set
{{(Center (Gauge (C,(i + 1)))),1},{(Center (Gauge (C,(i + 1))))}} is non empty set
Indices (Gauge (C,(i + 1))) is set
[(Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))] is set
{(Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))} is non empty V138() V139() V140() V141() V142() V143() set
{{(Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))},{(Center (Gauge (C,(i + 1))))}} is non empty set
len (Gauge (C,1)) is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) is compact Element of K6( the carrier of (TOP-REAL 2))
(Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
(Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))))) is connected compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) is compact Element of K6( the carrier of (TOP-REAL 2))
n is set
c9 is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
c9 `2 is V11() V12() ext-real Element of REAL
N-bound (L~ (Cage (C,(i + 1)))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (C,(i + 1)))) is strict compact SubSpace of TOP-REAL 2
proj2 | (L~ (Cage (C,(i + 1)))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,(i + 1)))))) V17( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,(i + 1))))), REAL ) V197((TOP-REAL 2) | (L~ (Cage (C,(i + 1))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,(i + 1))))),REAL))
the carrier of ((TOP-REAL 2) | (L~ (Cage (C,(i + 1))))) is set
K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,(i + 1))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,(i + 1))))),REAL)) is set
upper_bound (proj2 | (L~ (Cage (C,(i + 1))))) is V11() V12() ext-real Element of REAL
(proj2 | (L~ (Cage (C,(i + 1))))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (C,(i + 1))))) is V138() V139() V140() Element of K6(REAL)
upper_bound ((proj2 | (L~ (Cage (C,(i + 1))))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (C,(i + 1)))))) is V11() V12() ext-real Element of REAL
((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))) `2 is V11() V12() ext-real Element of REAL
S-bound (L~ (Cage (C,(i + 1)))) is V11() V12() ext-real Element of REAL
lower_bound (proj2 | (L~ (Cage (C,(i + 1))))) is V11() V12() ext-real Element of REAL
lower_bound ((proj2 | (L~ (Cage (C,(i + 1))))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (C,(i + 1)))))) is V11() V12() ext-real Element of REAL
((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)) `2 is V11() V12() ext-real Element of REAL
((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 is V11() V12() ext-real Element of REAL
((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))) `1 is V11() V12() ext-real Element of REAL
c9 `1 is V11() V12() ext-real Element of REAL
((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)) `1 is V11() V12() ext-real Element of REAL
((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))) `1 is V11() V12() ext-real Element of REAL
proj2 .: ((LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Lower_Seq (C,(i + 1))))) is V138() V139() V140() Element of K6(REAL)
lower_bound (proj2 .: ((LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Lower_Seq (C,(i + 1)))))) is V11() V12() ext-real Element of REAL
n is V6() V10() V11() V12() V37() ext-real non negative V76() V138() V139() V140() V141() V142() V143() Element of NAT
(Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n) is V33(2) FinSequence-like V130() Element of the carrier of (TOP-REAL 2)
((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n)) `2 is V11() V12() ext-real Element of REAL
((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 is V11() V12() ext-real Element of REAL
((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n)) `1 is V11() V12() ext-real Element of REAL
Upper_Seq (C,(i + 1)) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2)
L~ (Upper_Seq (C,(i + 1))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
Lower_Seq (C,(i + 1)) is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2)
L~ (Lower_Seq (C,(i + 1))) is non empty compact Element of K6( the carrier of (TOP-REAL 2))
Lower_Arc (L~ (Cage (C,(i + 1)))) is non empty Element of K6( the carrier of (TOP-REAL 2))