REAL is V150() V151() V152() V156() set
NAT is V150() V151() V152() V153() V154() V155() V156() Element of K6(REAL)
K6(REAL) is non empty set
COMPLEX is V150() V156() set
NAT is V150() V151() V152() V153() V154() V155() V156() set
K6(NAT) is non empty set
K6(NAT) is non empty set
1 is non empty V10() V11() V12() V26() ext-real positive non negative V103() V150() V151() V152() V153() V154() V155() Element of NAT
K7(1,1) is non empty set
K6(K7(1,1)) is non empty set
K7(K7(1,1),1) is non empty set
K6(K7(K7(1,1),1)) is non empty set
K7(K7(1,1),REAL) is set
K6(K7(K7(1,1),REAL)) is non empty set
K7(REAL,REAL) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is non empty set
2 is non empty V10() V11() V12() V26() ext-real positive non negative V103() V150() V151() V152() V153() V154() V155() Element of NAT
K7(2,2) is non empty set
K7(K7(2,2),REAL) is set
K6(K7(K7(2,2),REAL)) is non empty set
RAT is V150() V151() V152() V153() V156() set
INT is V150() V151() V152() V153() V154() V156() set
K6(K7(REAL,REAL)) is non empty set
TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V116() V162() V163() V164() V165() V166() V167() V168() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL 2) is non empty V21() set
K7( the carrier of (TOP-REAL 2),REAL) is set
K6(K7( the carrier of (TOP-REAL 2),REAL)) is non empty set
K6( the carrier of (TOP-REAL 2)) is non empty set
K456() is TopStruct
the carrier of K456() is set
RealSpace is strict MetrStruct
K461() is TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of K461() is set
K324( the carrier of (TOP-REAL 2)) is non empty V21() FinSequence-membered M11( the carrier of (TOP-REAL 2))
{} is empty V18() V21() FinSequence-membered V150() V151() V152() V153() V154() V155() V156() set
the empty V18() V21() FinSequence-membered V150() V151() V152() V153() V154() V155() V156() set is empty V18() V21() FinSequence-membered V150() V151() V152() V153() V154() V155() V156() set
3 is non empty V10() V11() V12() V26() ext-real positive non negative V103() V150() V151() V152() V153() V154() V155() Element of NAT
0 is empty V10() V11() V12() V18() V21() V26() FinSequence-membered ext-real non positive non negative V103() V150() V151() V152() V153() V154() V155() V156() Element of NAT
4 is non empty V10() V11() V12() V26() ext-real positive non negative V103() V150() V151() V152() V153() V154() V155() Element of NAT
R^2-unit_square is non empty non trivial V21() closed connected bounded being_special_polygon compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
C is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
C + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
x is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Y is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
n is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
[Y,n] is set
{Y,n} is non empty V150() V151() V152() V153() V154() V155() set
{Y} is non empty V150() V151() V152() V153() V154() V155() set
{{Y,n},{Y}} is non empty set
n + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
[Y,(n + 1)] is set
{Y,(n + 1)} is non empty V150() V151() V152() V153() V154() V155() set
{{Y,(n + 1)},{Y}} is non empty set
B is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Cage (B,x) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
len (Cage (B,x)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Gauge (B,x) is V13() V15() V16( NAT ) V17(K324( the carrier of (TOP-REAL 2))) V18() V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K324( the carrier of (TOP-REAL 2))
Indices (Gauge (B,x)) is set
(Cage (B,x)) /. C is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Gauge (B,x)) * (Y,n) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Cage (B,x)) /. (C + 1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Gauge (B,x)) * (Y,(n + 1)) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
len (Gauge (B,x)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
width (Gauge (B,x)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
right_cell ((Cage (B,x)),C,(Gauge (B,x))) is V21() Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (B,x)),Y,n) is V21() Element of K6( the carrier of (TOP-REAL 2))
C is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
C + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
x is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Y is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
n is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
[Y,n] is set
{Y,n} is non empty V150() V151() V152() V153() V154() V155() set
{Y} is non empty V150() V151() V152() V153() V154() V155() set
{{Y,n},{Y}} is non empty set
n + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
[Y,(n + 1)] is set
{Y,(n + 1)} is non empty V150() V151() V152() V153() V154() V155() set
{{Y,(n + 1)},{Y}} is non empty set
B is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Cage (B,x) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
len (Cage (B,x)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Gauge (B,x) is V13() V15() V16( NAT ) V17(K324( the carrier of (TOP-REAL 2))) V18() V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K324( the carrier of (TOP-REAL 2))
Indices (Gauge (B,x)) is set
(Cage (B,x)) /. C is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Gauge (B,x)) * (Y,(n + 1)) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Cage (B,x)) /. (C + 1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Gauge (B,x)) * (Y,n) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
Y -' 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
len (Gauge (B,x)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
width (Gauge (B,x)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
right_cell ((Cage (B,x)),C,(Gauge (B,x))) is V21() Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (B,x)),(Y -' 1),n) is V21() Element of K6( the carrier of (TOP-REAL 2))
C is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
C + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
x is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Y is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Y + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
n is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
[Y,n] is set
{Y,n} is non empty V150() V151() V152() V153() V154() V155() set
{Y} is non empty V150() V151() V152() V153() V154() V155() set
{{Y,n},{Y}} is non empty set
[(Y + 1),n] is set
{(Y + 1),n} is non empty V150() V151() V152() V153() V154() V155() set
{(Y + 1)} is non empty V150() V151() V152() V153() V154() V155() set
{{(Y + 1),n},{(Y + 1)}} is non empty set
B is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Cage (B,x) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
len (Cage (B,x)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Gauge (B,x) is V13() V15() V16( NAT ) V17(K324( the carrier of (TOP-REAL 2))) V18() V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K324( the carrier of (TOP-REAL 2))
Indices (Gauge (B,x)) is set
(Cage (B,x)) /. C is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Gauge (B,x)) * (Y,n) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Cage (B,x)) /. (C + 1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Gauge (B,x)) * ((Y + 1),n) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
n -' 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
len (Gauge (B,x)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
right_cell ((Cage (B,x)),C,(Gauge (B,x))) is V21() Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (B,x)),Y,(n -' 1)) is V21() Element of K6( the carrier of (TOP-REAL 2))
C is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
C + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
x is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Y is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Y + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
n is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
[Y,n] is set
{Y,n} is non empty V150() V151() V152() V153() V154() V155() set
{Y} is non empty V150() V151() V152() V153() V154() V155() set
{{Y,n},{Y}} is non empty set
[(Y + 1),n] is set
{(Y + 1),n} is non empty V150() V151() V152() V153() V154() V155() set
{(Y + 1)} is non empty V150() V151() V152() V153() V154() V155() set
{{(Y + 1),n},{(Y + 1)}} is non empty set
B is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Cage (B,x) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
len (Cage (B,x)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Gauge (B,x) is V13() V15() V16( NAT ) V17(K324( the carrier of (TOP-REAL 2))) V18() V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K324( the carrier of (TOP-REAL 2))
Indices (Gauge (B,x)) is set
(Cage (B,x)) /. C is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Gauge (B,x)) * ((Y + 1),n) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Cage (B,x)) /. (C + 1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Gauge (B,x)) * (Y,n) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
width (Gauge (B,x)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
len (Gauge (B,x)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
right_cell ((Cage (B,x)),C,(Gauge (B,x))) is V21() Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (B,x)),Y,n) is V21() Element of K6( the carrier of (TOP-REAL 2))
C is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
x is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Cage (x,C) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (x,C)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
Gauge (x,C) is V13() V15() V16( NAT ) V17(K324( the carrier of (TOP-REAL 2))) V18() V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K324( the carrier of (TOP-REAL 2))
B is set
len (Cage (x,C)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
{ (LSeg ((Cage (x,C)),b1)) where b1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (Cage (x,C)) ) } is set
union { (LSeg ((Cage (x,C)),b1)) where b1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (Cage (x,C)) ) } is set
P is set
f is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
LSeg ((Cage (x,C)),f) is V21() Element of K6( the carrier of (TOP-REAL 2))
f + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
left_cell ((Cage (x,C)),f,(Gauge (x,C))) is V21() Element of K6( the carrier of (TOP-REAL 2))
right_cell ((Cage (x,C)),f,(Gauge (x,C))) is V21() Element of K6( the carrier of (TOP-REAL 2))
(left_cell ((Cage (x,C)),f,(Gauge (x,C)))) /\ (right_cell ((Cage (x,C)),f,(Gauge (x,C)))) is V21() Element of K6( the carrier of (TOP-REAL 2))
C is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
2 |^ C is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
x is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Cage (x,C) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (x,C)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
N-bound (L~ (Cage (x,C))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (x,C))) is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj2 is V13() V16( the carrier of (TOP-REAL 2)) V17( REAL ) V18() V40( the carrier of (TOP-REAL 2), REAL ) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
proj2 | (L~ (Cage (x,C))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (x,C))))) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (x,C)))), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (x,C)))),REAL))
the carrier of ((TOP-REAL 2) | (L~ (Cage (x,C)))) is non empty set
K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (x,C)))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (x,C)))),REAL)) is non empty set
K360(((TOP-REAL 2) | (L~ (Cage (x,C)))),(proj2 | (L~ (Cage (x,C))))) is V11() V12() ext-real Element of REAL
N-bound x is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | x is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj2 | x is V13() V16( the carrier of ((TOP-REAL 2) | x)) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | x), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | x),REAL))
the carrier of ((TOP-REAL 2) | x) is non empty set
K7( the carrier of ((TOP-REAL 2) | x),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | x),REAL)) is non empty set
K360(((TOP-REAL 2) | x),(proj2 | x)) is V11() V12() ext-real Element of REAL
S-bound x is V11() V12() ext-real Element of REAL
K359(((TOP-REAL 2) | x),(proj2 | x)) is V11() V12() ext-real Element of REAL
(N-bound x) - (S-bound x) is V11() V12() ext-real Element of REAL
((N-bound x) - (S-bound x)) / (2 |^ C) is V11() V12() ext-real Element of REAL
(N-bound x) + (((N-bound x) - (S-bound x)) / (2 |^ C)) is V11() V12() ext-real Element of REAL
W-bound x is V11() V12() ext-real Element of REAL
proj1 is V13() V16( the carrier of (TOP-REAL 2)) V17( REAL ) V18() V40( the carrier of (TOP-REAL 2), REAL ) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
proj1 | x is V13() V16( the carrier of ((TOP-REAL 2) | x)) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | x), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | x),REAL))
K359(((TOP-REAL 2) | x),(proj1 | x)) is V11() V12() ext-real Element of REAL
Gauge (x,C) is V13() V15() V16( NAT ) V17(K324( the carrier of (TOP-REAL 2))) V18() V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K324( the carrier of (TOP-REAL 2))
len (Gauge (x,C)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
(Cage (x,C)) /. 1 is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
width (Gauge (x,C)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
(Cage (x,C)) /. 2 is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
N-min x is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
N-most x is V21() Element of K6( the carrier of (TOP-REAL 2))
NW-corner x is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
|[(W-bound x),(N-bound x)]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
NE-corner x is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
E-bound x is V11() V12() ext-real Element of REAL
K360(((TOP-REAL 2) | x),(proj1 | x)) is V11() V12() ext-real Element of REAL
|[(E-bound x),(N-bound x)]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
LSeg ((NW-corner x),(NE-corner x)) is V21() closed closed boundary connected bounded bounded compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((NW-corner x),(NE-corner x))) /\ x is V21() Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (N-most x) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 | (N-most x) is V13() V16( the carrier of ((TOP-REAL 2) | (N-most x))) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | (N-most x)), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (N-most x)),REAL))
the carrier of ((TOP-REAL 2) | (N-most x)) is set
K7( the carrier of ((TOP-REAL 2) | (N-most x)),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (N-most x)),REAL)) is non empty set
K359(((TOP-REAL 2) | (N-most x)),(proj1 | (N-most x))) is V11() V12() ext-real Element of REAL
|[K359(((TOP-REAL 2) | (N-most x)),(proj1 | (N-most x))),(N-bound x)]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(width (Gauge (x,C))) -' 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
f is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
f + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
(Gauge (x,C)) * (f,(width (Gauge (x,C)))) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Gauge (x,C)) * ((f + 1),(width (Gauge (x,C)))) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
cell ((Gauge (x,C)),f,((width (Gauge (x,C))) -' 1)) is V21() Element of K6( the carrier of (TOP-REAL 2))
(Gauge (x,C)) * (f,((width (Gauge (x,C))) -' 1)) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
f + 0 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
[f,(len (Gauge (x,C)))] is set
{f,(len (Gauge (x,C)))} is non empty V150() V151() V152() V153() V154() V155() set
{f} is non empty V150() V151() V152() V153() V154() V155() set
{{f,(len (Gauge (x,C)))},{f}} is non empty set
Indices (Gauge (x,C)) is set
N-min (L~ (Cage (x,C))) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
N-most (L~ (Cage (x,C))) is V21() Element of K6( the carrier of (TOP-REAL 2))
NW-corner (L~ (Cage (x,C))) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
W-bound (L~ (Cage (x,C))) is V11() V12() ext-real Element of REAL
proj1 | (L~ (Cage (x,C))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (x,C))))) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (x,C)))), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (x,C)))),REAL))
K359(((TOP-REAL 2) | (L~ (Cage (x,C)))),(proj1 | (L~ (Cage (x,C))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (x,C)))),(N-bound (L~ (Cage (x,C))))]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
NE-corner (L~ (Cage (x,C))) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
E-bound (L~ (Cage (x,C))) is V11() V12() ext-real Element of REAL
K360(((TOP-REAL 2) | (L~ (Cage (x,C)))),(proj1 | (L~ (Cage (x,C))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (x,C)))),(N-bound (L~ (Cage (x,C))))]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
LSeg ((NW-corner (L~ (Cage (x,C)))),(NE-corner (L~ (Cage (x,C))))) is V21() closed closed boundary connected bounded bounded compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((NW-corner (L~ (Cage (x,C)))),(NE-corner (L~ (Cage (x,C)))))) /\ (L~ (Cage (x,C))) is V21() Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (N-most (L~ (Cage (x,C)))) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 | (N-most (L~ (Cage (x,C)))) is V13() V16( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (x,C)))))) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (x,C))))), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (x,C))))),REAL))
the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (x,C))))) is set
K7( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (x,C))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (x,C))))),REAL)) is non empty set
K359(((TOP-REAL 2) | (N-most (L~ (Cage (x,C))))),(proj1 | (N-most (L~ (Cage (x,C)))))) is V11() V12() ext-real Element of REAL
|[K359(((TOP-REAL 2) | (N-most (L~ (Cage (x,C))))),(proj1 | (N-most (L~ (Cage (x,C)))))),(N-bound (L~ (Cage (x,C))))]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(N-min (L~ (Cage (x,C)))) `2 is V11() V12() ext-real Element of REAL
((Cage (x,C)) /. 1) `2 is V11() V12() ext-real Element of REAL
(E-bound x) - (W-bound x) is V11() V12() ext-real Element of REAL
((E-bound x) - (W-bound x)) / (2 |^ C) is V11() V12() ext-real Element of REAL
f - 2 is V11() V12() ext-real Element of REAL
(((E-bound x) - (W-bound x)) / (2 |^ C)) * (f - 2) is V11() V12() ext-real Element of REAL
(W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ C)) * (f - 2)) is V11() V12() ext-real Element of REAL
(len (Gauge (x,C))) - 2 is V11() V12() ext-real Element of REAL
(((N-bound x) - (S-bound x)) / (2 |^ C)) * ((len (Gauge (x,C))) - 2) is V11() V12() ext-real Element of REAL
(S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ C)) * ((len (Gauge (x,C))) - 2)) is V11() V12() ext-real Element of REAL
|[((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ C)) * (f - 2))),((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ C)) * ((len (Gauge (x,C))) - 2)))]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
|[((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ C)) * (f - 2))),((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ C)) * ((len (Gauge (x,C))) - 2)))]| `2 is V11() V12() ext-real Element of REAL
(2 |^ C) + 3 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
((2 |^ C) + 3) - 2 is V11() V12() ext-real Element of REAL
(((N-bound x) - (S-bound x)) / (2 |^ C)) * (((2 |^ C) + 3) - 2) is V11() V12() ext-real Element of REAL
(S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ C)) * (((2 |^ C) + 3) - 2)) is V11() V12() ext-real Element of REAL
(((N-bound x) - (S-bound x)) / (2 |^ C)) * (2 |^ C) is V11() V12() ext-real Element of REAL
(S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ C)) * (2 |^ C)) is V11() V12() ext-real Element of REAL
((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ C)) * (2 |^ C))) + (((N-bound x) - (S-bound x)) / (2 |^ C)) is V11() V12() ext-real Element of REAL
(S-bound x) + ((N-bound x) - (S-bound x)) is V11() V12() ext-real Element of REAL
((S-bound x) + ((N-bound x) - (S-bound x))) + (((N-bound x) - (S-bound x)) / (2 |^ C)) is V11() V12() ext-real Element of REAL
C is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
x is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Y is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Cage (Y,C) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (Y,C)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
N-bound (L~ (Cage (Y,C))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (Y,C))) is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj2 is V13() V16( the carrier of (TOP-REAL 2)) V17( REAL ) V18() V40( the carrier of (TOP-REAL 2), REAL ) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
proj2 | (L~ (Cage (Y,C))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,C))))) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,C)))), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,C)))),REAL))
the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,C)))) is non empty set
K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,C)))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,C)))),REAL)) is non empty set
K360(((TOP-REAL 2) | (L~ (Cage (Y,C)))),(proj2 | (L~ (Cage (Y,C))))) is V11() V12() ext-real Element of REAL
Cage (Y,x) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (Y,x)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
N-bound (L~ (Cage (Y,x))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (Y,x))) is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj2 | (L~ (Cage (Y,x))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,x))))) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,x)))), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,x)))),REAL))
the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,x)))) is non empty set
K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,x)))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,x)))),REAL)) is non empty set
K360(((TOP-REAL 2) | (L~ (Cage (Y,x)))),(proj2 | (L~ (Cage (Y,x))))) is V11() V12() ext-real Element of REAL
n is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Cage (Y,n) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (Y,n)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
N-bound (L~ (Cage (Y,n))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (Y,n))) is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj2 | (L~ (Cage (Y,n))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,n))))) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,n)))), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,n)))),REAL))
the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,n)))) is non empty set
K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,n)))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,n)))),REAL)) is non empty set
K360(((TOP-REAL 2) | (L~ (Cage (Y,n)))),(proj2 | (L~ (Cage (Y,n))))) is V11() V12() ext-real Element of REAL
n + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Cage (Y,(n + 1)) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (Y,(n + 1))) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
N-bound (L~ (Cage (Y,(n + 1)))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (Y,(n + 1)))) is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj2 | (L~ (Cage (Y,(n + 1)))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,(n + 1)))))) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,(n + 1))))), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,(n + 1))))),REAL))
the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,(n + 1))))) is non empty set
K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,(n + 1))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,(n + 1))))),REAL)) is non empty set
K360(((TOP-REAL 2) | (L~ (Cage (Y,(n + 1))))),(proj2 | (L~ (Cage (Y,(n + 1)))))) is V11() V12() ext-real Element of REAL
N-bound Y is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | Y is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj2 | Y is V13() V16( the carrier of ((TOP-REAL 2) | Y)) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | Y), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | Y),REAL))
the carrier of ((TOP-REAL 2) | Y) is non empty set
K7( the carrier of ((TOP-REAL 2) | Y),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | Y),REAL)) is non empty set
K360(((TOP-REAL 2) | Y),(proj2 | Y)) is V11() V12() ext-real Element of REAL
S-bound Y is V11() V12() ext-real Element of REAL
K359(((TOP-REAL 2) | Y),(proj2 | Y)) is V11() V12() ext-real Element of REAL
(N-bound Y) - (S-bound Y) is V11() V12() ext-real Element of REAL
2 |^ (n + 1) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
((N-bound Y) - (S-bound Y)) / (2 |^ (n + 1)) is V11() V12() ext-real Element of REAL
(N-bound Y) + (((N-bound Y) - (S-bound Y)) / (2 |^ (n + 1))) is V11() V12() ext-real Element of REAL
2 |^ n is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
((N-bound Y) - (S-bound Y)) / (2 |^ n) is V11() V12() ext-real Element of REAL
(N-bound Y) + (((N-bound Y) - (S-bound Y)) / (2 |^ n)) is V11() V12() ext-real Element of REAL
((N-bound Y) + (((N-bound Y) - (S-bound Y)) / (2 |^ (n + 1)))) - ((N-bound Y) + (((N-bound Y) - (S-bound Y)) / (2 |^ n))) is V11() V12() ext-real Element of REAL
0 + (((N-bound Y) - (S-bound Y)) / (2 |^ (n + 1))) is V11() V12() ext-real Element of REAL
(0 + (((N-bound Y) - (S-bound Y)) / (2 |^ (n + 1)))) - (((N-bound Y) - (S-bound Y)) / (2 |^ n)) is V11() V12() ext-real Element of REAL
(2 |^ n) * 2 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
((N-bound Y) - (S-bound Y)) / ((2 |^ n) * 2) is V11() V12() ext-real Element of REAL
2 / 2 is V11() V12() ext-real Element of REAL
(((N-bound Y) - (S-bound Y)) / (2 |^ n)) / (2 / 2) is V11() V12() ext-real Element of REAL
(((N-bound Y) - (S-bound Y)) / ((2 |^ n) * 2)) - ((((N-bound Y) - (S-bound Y)) / (2 |^ n)) / (2 / 2)) is V11() V12() ext-real Element of REAL
((N-bound Y) - (S-bound Y)) * 2 is V11() V12() ext-real Element of REAL
(((N-bound Y) - (S-bound Y)) * 2) / ((2 |^ n) * 2) is V11() V12() ext-real Element of REAL
(((N-bound Y) - (S-bound Y)) / ((2 |^ n) * 2)) - ((((N-bound Y) - (S-bound Y)) * 2) / ((2 |^ n) * 2)) is V11() V12() ext-real Element of REAL
2 * (N-bound Y) is V11() V12() ext-real Element of REAL
2 * (S-bound Y) is V11() V12() ext-real Element of REAL
(2 * (N-bound Y)) - (2 * (S-bound Y)) is V11() V12() ext-real Element of REAL
((N-bound Y) - (S-bound Y)) - ((2 * (N-bound Y)) - (2 * (S-bound Y))) is V11() V12() ext-real Element of REAL
(((N-bound Y) - (S-bound Y)) - ((2 * (N-bound Y)) - (2 * (S-bound Y)))) / ((2 |^ n) * 2) is V11() V12() ext-real Element of REAL
(S-bound Y) - (N-bound Y) is V11() V12() ext-real Element of REAL
((S-bound Y) - (N-bound Y)) / ((2 |^ n) * 2) is V11() V12() ext-real Element of REAL
0 * 2 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Cage (Y,0) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (Y,0)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
N-bound (L~ (Cage (Y,0))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (Y,0))) is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj2 | (L~ (Cage (Y,0))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,0))))) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,0)))), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,0)))),REAL))
the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,0)))) is non empty set
K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,0)))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (Y,0)))),REAL)) is non empty set
K360(((TOP-REAL 2) | (L~ (Cage (Y,0)))),(proj2 | (L~ (Cage (Y,0))))) is V11() V12() ext-real Element of REAL
C is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
x is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Cage (C,x) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
RightComp (Cage (C,x)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
Cl (RightComp (Cage (C,x))) is V21() Element of K6( the carrier of (TOP-REAL 2))
C is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
x is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
N-min x is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
N-most x is V21() Element of K6( the carrier of (TOP-REAL 2))
NW-corner x is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
W-bound x is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | x is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 is V13() V16( the carrier of (TOP-REAL 2)) V17( REAL ) V18() V40( the carrier of (TOP-REAL 2), REAL ) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
proj1 | x is V13() V16( the carrier of ((TOP-REAL 2) | x)) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | x), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | x),REAL))
the carrier of ((TOP-REAL 2) | x) is non empty set
K7( the carrier of ((TOP-REAL 2) | x),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | x),REAL)) is non empty set
K359(((TOP-REAL 2) | x),(proj1 | x)) is V11() V12() ext-real Element of REAL
N-bound x is V11() V12() ext-real Element of REAL
proj2 is V13() V16( the carrier of (TOP-REAL 2)) V17( REAL ) V18() V40( the carrier of (TOP-REAL 2), REAL ) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
proj2 | x is V13() V16( the carrier of ((TOP-REAL 2) | x)) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | x), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | x),REAL))
K360(((TOP-REAL 2) | x),(proj2 | x)) is V11() V12() ext-real Element of REAL
|[(W-bound x),(N-bound x)]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
NE-corner x is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
E-bound x is V11() V12() ext-real Element of REAL
K360(((TOP-REAL 2) | x),(proj1 | x)) is V11() V12() ext-real Element of REAL
|[(E-bound x),(N-bound x)]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
LSeg ((NW-corner x),(NE-corner x)) is V21() closed closed boundary connected bounded bounded compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((NW-corner x),(NE-corner x))) /\ x is V21() Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (N-most x) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 | (N-most x) is V13() V16( the carrier of ((TOP-REAL 2) | (N-most x))) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | (N-most x)), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (N-most x)),REAL))
the carrier of ((TOP-REAL 2) | (N-most x)) is set
K7( the carrier of ((TOP-REAL 2) | (N-most x)),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (N-most x)),REAL)) is non empty set
K359(((TOP-REAL 2) | (N-most x)),(proj1 | (N-most x))) is V11() V12() ext-real Element of REAL
|[K359(((TOP-REAL 2) | (N-most x)),(proj1 | (N-most x))),(N-bound x)]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
Cage (x,C) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
RightComp (Cage (x,C)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
Gauge (x,C) is V13() V15() V16( NAT ) V17(K324( the carrier of (TOP-REAL 2))) V18() V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K324( the carrier of (TOP-REAL 2))
len (Gauge (x,C)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
(Cage (x,C)) /. 1 is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
width (Gauge (x,C)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
(Cage (x,C)) /. 2 is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(width (Gauge (x,C))) -' 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
B is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
B + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
(Gauge (x,C)) * (B,(width (Gauge (x,C)))) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Gauge (x,C)) * ((B + 1),(width (Gauge (x,C)))) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
cell ((Gauge (x,C)),B,((width (Gauge (x,C))) -' 1)) is V21() Element of K6( the carrier of (TOP-REAL 2))
(Gauge (x,C)) * (B,((width (Gauge (x,C))) -' 1)) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
[(B + 1),(len (Gauge (x,C)))] is set
{(B + 1),(len (Gauge (x,C)))} is non empty V150() V151() V152() V153() V154() V155() set
{(B + 1)} is non empty V150() V151() V152() V153() V154() V155() set
{{(B + 1),(len (Gauge (x,C)))},{(B + 1)}} is non empty set
Indices (Gauge (x,C)) is set
L~ (Cage (x,C)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
1 + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
len (Cage (x,C)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
right_cell ((Cage (x,C)),1,(Gauge (x,C))) is V21() Element of K6( the carrier of (TOP-REAL 2))
Fr (right_cell ((Cage (x,C)),1,(Gauge (x,C)))) is V21() Element of K6( the carrier of (TOP-REAL 2))
Int (right_cell ((Cage (x,C)),1,(Gauge (x,C)))) is V21() Element of K6( the carrier of (TOP-REAL 2))
(right_cell ((Cage (x,C)),1,(Gauge (x,C)))) \ (Int (right_cell ((Cage (x,C)),1,(Gauge (x,C))))) is V21() Element of K6( the carrier of (TOP-REAL 2))
(Fr (right_cell ((Cage (x,C)),1,(Gauge (x,C))))) \/ (Int (right_cell ((Cage (x,C)),1,(Gauge (x,C))))) is V21() Element of K6( the carrier of (TOP-REAL 2))
[B,(len (Gauge (x,C)))] is set
{B,(len (Gauge (x,C)))} is non empty V150() V151() V152() V153() V154() V155() set
{B} is non empty V150() V151() V152() V153() V154() V155() set
{{B,(len (Gauge (x,C)))},{B}} is non empty set
(len (Gauge (x,C))) -' 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
cell ((Gauge (x,C)),B,((len (Gauge (x,C))) -' 1)) is V21() Element of K6( the carrier of (TOP-REAL 2))
right_cell ((Cage (x,C)),1) is V21() Element of K6( the carrier of (TOP-REAL 2))
Int (right_cell ((Cage (x,C)),1)) is V21() Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((Gauge (x,C)),B,((len (Gauge (x,C))) -' 1))) is V21() Element of K6( the carrier of (TOP-REAL 2))
(RightComp (Cage (x,C))) /\ (L~ (Cage (x,C))) is V21() Element of K6( the carrier of (TOP-REAL 2))
Fr (cell ((Gauge (x,C)),B,((len (Gauge (x,C))) -' 1))) is V21() Element of K6( the carrier of (TOP-REAL 2))
(RightComp (Cage (x,C))) \/ (L~ (Cage (x,C))) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
P is set
4 - 1 is V11() V12() ext-real Element of REAL
(len (Gauge (x,C))) - 1 is V11() V12() ext-real Element of REAL
(len (Gauge (x,C))) - 0 is V11() V12() ext-real Element of REAL
f is set
P1 is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
f is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
LSeg (P1,f) is V21() closed closed boundary connected bounded bounded compact compact Element of K6( the carrier of (TOP-REAL 2))
(L~ (Cage (x,C))) ` is V21() Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ (Cage (x,C))) is set
(Gauge (x,C)) * (B,1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
((Gauge (x,C)) * (B,1)) `1 is V11() V12() ext-real Element of REAL
(Gauge (x,C)) * ((B + 1),1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
((Gauge (x,C)) * ((B + 1),1)) `1 is V11() V12() ext-real Element of REAL
(Gauge (x,C)) * (1,((len (Gauge (x,C))) -' 1)) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
((Gauge (x,C)) * (1,((len (Gauge (x,C))) -' 1))) `2 is V11() V12() ext-real Element of REAL
((len (Gauge (x,C))) -' 1) + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
(Gauge (x,C)) * (1,(((len (Gauge (x,C))) -' 1) + 1)) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
((Gauge (x,C)) * (1,(((len (Gauge (x,C))) -' 1) + 1))) `2 is V11() V12() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() V12() ext-real Element of REAL : ( not b1 <= ((Gauge (x,C)) * (B,1)) `1 & not ((Gauge (x,C)) * ((B + 1),1)) `1 <= b1 & not b2 <= ((Gauge (x,C)) * (1,((len (Gauge (x,C))) -' 1))) `2 & not ((Gauge (x,C)) * (1,(((len (Gauge (x,C))) -' 1) + 1))) `2 <= b2 ) } is set
{ |[b1,b2]| where b1, b2 is V11() V12() ext-real Element of REAL : ( ((Gauge (x,C)) * (B,1)) `1 <= b1 & b1 <= ((Gauge (x,C)) * ((B + 1),1)) `1 & ((Gauge (x,C)) * (1,((len (Gauge (x,C))) -' 1))) `2 <= b2 & b2 <= ((Gauge (x,C)) * (1,(((len (Gauge (x,C))) -' 1) + 1))) `2 ) } is set
C1 is V11() V12() ext-real Element of REAL
d is V11() V12() ext-real Element of REAL
|[C1,d]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
f `2 is V11() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
G is V11() V12() ext-real Element of REAL
|[n,G]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
P1 `1 is V11() V12() ext-real Element of REAL
g is set
a is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
a `1 is V11() V12() ext-real Element of REAL
a `2 is V11() V12() ext-real Element of REAL
|[(a `1),(a `2)]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
P1 `2 is V11() V12() ext-real Element of REAL
f `1 is V11() V12() ext-real Element of REAL
{P1} is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
C1 is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
{P1} is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
C1 is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
x /\ (L~ (Cage (x,C))) is V21() Element of K6( the carrier of (TOP-REAL 2))
C is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
x is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Cage (x,C) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
RightComp (Cage (x,C)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
N-min x is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
N-most x is V21() Element of K6( the carrier of (TOP-REAL 2))
NW-corner x is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
W-bound x is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | x is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 is V13() V16( the carrier of (TOP-REAL 2)) V17( REAL ) V18() V40( the carrier of (TOP-REAL 2), REAL ) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
proj1 | x is V13() V16( the carrier of ((TOP-REAL 2) | x)) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | x), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | x),REAL))
the carrier of ((TOP-REAL 2) | x) is non empty set
K7( the carrier of ((TOP-REAL 2) | x),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | x),REAL)) is non empty set
K359(((TOP-REAL 2) | x),(proj1 | x)) is V11() V12() ext-real Element of REAL
N-bound x is V11() V12() ext-real Element of REAL
proj2 is V13() V16( the carrier of (TOP-REAL 2)) V17( REAL ) V18() V40( the carrier of (TOP-REAL 2), REAL ) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
proj2 | x is V13() V16( the carrier of ((TOP-REAL 2) | x)) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | x), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | x),REAL))
K360(((TOP-REAL 2) | x),(proj2 | x)) is V11() V12() ext-real Element of REAL
|[(W-bound x),(N-bound x)]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
NE-corner x is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
E-bound x is V11() V12() ext-real Element of REAL
K360(((TOP-REAL 2) | x),(proj1 | x)) is V11() V12() ext-real Element of REAL
|[(E-bound x),(N-bound x)]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
LSeg ((NW-corner x),(NE-corner x)) is V21() closed closed boundary connected bounded bounded compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((NW-corner x),(NE-corner x))) /\ x is V21() Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (N-most x) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 | (N-most x) is V13() V16( the carrier of ((TOP-REAL 2) | (N-most x))) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | (N-most x)), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (N-most x)),REAL))
the carrier of ((TOP-REAL 2) | (N-most x)) is set
K7( the carrier of ((TOP-REAL 2) | (N-most x)),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (N-most x)),REAL)) is non empty set
K359(((TOP-REAL 2) | (N-most x)),(proj1 | (N-most x))) is V11() V12() ext-real Element of REAL
|[K359(((TOP-REAL 2) | (N-most x)),(proj1 | (N-most x))),(N-bound x)]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
x /\ (RightComp (Cage (x,C))) is V21() Element of K6( the carrier of (TOP-REAL 2))
C is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
x is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Cage (x,C) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
LeftComp (Cage (x,C)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
L~ (Cage (x,C)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
(L~ (Cage (x,C))) ` is V21() Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ (Cage (x,C))) is set
RightComp (Cage (x,C)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | ((L~ (Cage (x,C))) `) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | ((L~ (Cage (x,C))) `)) is set
K6( the carrier of ((TOP-REAL 2) | ((L~ (Cage (x,C))) `))) is non empty set
x /\ (L~ (Cage (x,C))) is V21() Element of K6( the carrier of (TOP-REAL 2))
n is set
n is Element of K6( the carrier of ((TOP-REAL 2) | ((L~ (Cage (x,C))) `)))
B is Element of K6( the carrier of ((TOP-REAL 2) | ((L~ (Cage (x,C))) `)))
P is Element of K6( the carrier of ((TOP-REAL 2) | ((L~ (Cage (x,C))) `)))
C is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
x is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Cage (x,C) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
RightComp (Cage (x,C)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
n is set
L~ (Cage (x,C)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
x /\ (L~ (Cage (x,C))) is V21() Element of K6( the carrier of (TOP-REAL 2))
LeftComp (Cage (x,C)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
x /\ (LeftComp (Cage (x,C))) is V21() Element of K6( the carrier of (TOP-REAL 2))
C is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
x is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Cage (x,C) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (x,C)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Cage (x,C))) is V21() open Element of K6( the carrier of (TOP-REAL 2))
RightComp (Cage (x,C)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
C is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
x is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Cage (x,C) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (x,C)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
UBD (L~ (Cage (x,C))) is non empty V21() open connected being_Region Element of K6( the carrier of (TOP-REAL 2))
UBD x is non empty V21() open connected being_Region Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V21() Element of K6( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of x } is set
union { b1 where b1 is V21() Element of K6( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of x } is set
n is set
{ b1 where b1 is V21() Element of K6( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of L~ (Cage (x,C)) } is set
union { b1 where b1 is V21() Element of K6( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of L~ (Cage (x,C)) } is set
B is set
P is V21() Element of K6( the carrier of (TOP-REAL 2))
Euclid 2 is non empty strict Reflexive discerning symmetric triangle MetrStruct
the carrier of (Euclid 2) is non empty set
K6( the carrier of (Euclid 2)) is non empty set
f is Element of K6( the carrier of (Euclid 2))
RightComp (Cage (x,C)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
f /\ (RightComp (Cage (x,C))) is V21() Element of K6( the carrier of (TOP-REAL 2))
x ` is V21() Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ x is set
(TOP-REAL 2) | (x `) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (x `)) is set
Down (P,(x `)) is Element of K6( the carrier of ((TOP-REAL 2) | (x `)))
K6( the carrier of ((TOP-REAL 2) | (x `))) is non empty set
P /\ (x `) is V21() Element of K6( the carrier of (TOP-REAL 2))
Component_of (Down (P,(x `))) is Element of K6( the carrier of ((TOP-REAL 2) | (x `)))
(L~ (Cage (x,C))) ` is V21() Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ (Cage (x,C))) is set
(TOP-REAL 2) | ((L~ (Cage (x,C))) `) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | ((L~ (Cage (x,C))) `)) is set
K6( the carrier of ((TOP-REAL 2) | ((L~ (Cage (x,C))) `))) is non empty set
P1 is Element of K6( the carrier of ((TOP-REAL 2) | ((L~ (Cage (x,C))) `)))
f is V21() Element of K6( the carrier of (TOP-REAL 2))
C1 is set
C is non empty V21() closed bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
{ (UBD (L~ (Cage (C,b1)))) where b1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT : verum } is set
{ (Cl (BDD (L~ (Cage (C,b1))))) where b1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT : verum } is set
C is non empty V21() closed bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
(C) is set
{ (UBD (L~ (Cage (C,b1)))) where b1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT : verum } is set
K6(K6( the carrier of (TOP-REAL 2))) is non empty set
bool the carrier of (TOP-REAL 2) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))
x is set
Y is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Cage (C,Y) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,Y)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
UBD (L~ (Cage (C,Y))) is non empty V21() open connected being_Region Element of K6( the carrier of (TOP-REAL 2))
(C) is set
{ (Cl (BDD (L~ (Cage (C,b1))))) where b1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT : verum } is set
bool the carrier of (TOP-REAL 2) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))
x is set
Y is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Cage (C,Y) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,Y)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Cage (C,Y))) is V21() open Element of K6( the carrier of (TOP-REAL 2))
Cl (BDD (L~ (Cage (C,Y)))) is V21() Element of K6( the carrier of (TOP-REAL 2))
C is non empty V21() closed bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
(C) is Element of K6(K6( the carrier of (TOP-REAL 2)))
{ (UBD (L~ (Cage (C,b1)))) where b1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT : verum } is set
Cage (C,0) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,0)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
UBD (L~ (Cage (C,0))) is non empty V21() open connected being_Region Element of K6( the carrier of (TOP-REAL 2))
(C) is Element of K6(K6( the carrier of (TOP-REAL 2)))
{ (Cl (BDD (L~ (Cage (C,b1))))) where b1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT : verum } is set
Cage (C,0) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,0)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Cage (C,0))) is V21() open Element of K6( the carrier of (TOP-REAL 2))
Cl (BDD (L~ (Cage (C,0)))) is V21() Element of K6( the carrier of (TOP-REAL 2))
C is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
(C) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))
{ (UBD (L~ (Cage (C,b1)))) where b1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT : verum } is set
union (C) is V21() Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty V21() open connected being_Region Element of K6( the carrier of (TOP-REAL 2))
Cage (C,0) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,0)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
UBD (L~ (Cage (C,0))) is non empty V21() open connected being_Region Element of K6( the carrier of (TOP-REAL 2))
LeftComp (Cage (C,0)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
x is set
Y is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Cage (C,Y) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,Y)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
UBD (L~ (Cage (C,Y))) is non empty V21() open connected being_Region Element of K6( the carrier of (TOP-REAL 2))
x is set
{ b1 where b1 is V21() Element of K6( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of C } is set
union { b1 where b1 is V21() Element of K6( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of C } is set
Y is set
B is V21() Element of K6( the carrier of (TOP-REAL 2))
N-bound (L~ (Cage (C,0))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (C,0))) is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj2 is V13() V16( the carrier of (TOP-REAL 2)) V17( REAL ) V18() V40( the carrier of (TOP-REAL 2), REAL ) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
proj2 | (L~ (Cage (C,0))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,0))))) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,0)))), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,0)))),REAL))
the carrier of ((TOP-REAL 2) | (L~ (Cage (C,0)))) is non empty set
K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,0)))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,0)))),REAL)) is non empty set
K360(((TOP-REAL 2) | (L~ (Cage (C,0)))),(proj2 | (L~ (Cage (C,0))))) is V11() V12() ext-real Element of REAL
n is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
B is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
B `2 is V11() V12() ext-real Element of REAL
(Cage (C,0)) /. 1 is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
N-min (L~ (Cage (C,0))) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
N-most (L~ (Cage (C,0))) is V21() Element of K6( the carrier of (TOP-REAL 2))
NW-corner (L~ (Cage (C,0))) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
W-bound (L~ (Cage (C,0))) is V11() V12() ext-real Element of REAL
proj1 is V13() V16( the carrier of (TOP-REAL 2)) V17( REAL ) V18() V40( the carrier of (TOP-REAL 2), REAL ) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
proj1 | (L~ (Cage (C,0))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,0))))) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,0)))), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,0)))),REAL))
K359(((TOP-REAL 2) | (L~ (Cage (C,0)))),(proj1 | (L~ (Cage (C,0))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (C,0)))),(N-bound (L~ (Cage (C,0))))]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
NE-corner (L~ (Cage (C,0))) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
E-bound (L~ (Cage (C,0))) is V11() V12() ext-real Element of REAL
K360(((TOP-REAL 2) | (L~ (Cage (C,0)))),(proj1 | (L~ (Cage (C,0))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (C,0)))),(N-bound (L~ (Cage (C,0))))]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
LSeg ((NW-corner (L~ (Cage (C,0)))),(NE-corner (L~ (Cage (C,0))))) is V21() closed closed boundary connected bounded bounded compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((NW-corner (L~ (Cage (C,0)))),(NE-corner (L~ (Cage (C,0)))))) /\ (L~ (Cage (C,0))) is V21() Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (N-most (L~ (Cage (C,0)))) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 | (N-most (L~ (Cage (C,0)))) is V13() V16( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (C,0)))))) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (C,0))))), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (C,0))))),REAL))
the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (C,0))))) is set
K7( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (C,0))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (C,0))))),REAL)) is non empty set
K359(((TOP-REAL 2) | (N-most (L~ (Cage (C,0))))),(proj1 | (N-most (L~ (Cage (C,0)))))) is V11() V12() ext-real Element of REAL
|[K359(((TOP-REAL 2) | (N-most (L~ (Cage (C,0))))),(proj1 | (N-most (L~ (Cage (C,0)))))),(N-bound (L~ (Cage (C,0))))]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
P is V21() Element of K6( the carrier of (TOP-REAL 2))
f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f is V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
f /. 1 is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
len f is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
f /. (len f) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
f is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V19() V28() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2)
len f is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
L~ f is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
the topology of (TOP-REAL 2) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is non empty strict TopSpace-like TopStruct
Euclid 2 is non empty strict Reflexive discerning symmetric triangle MetrStruct
TopSpaceMetr (Euclid 2) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid 2)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is non empty set
P1 is non empty compact Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
C1 is non empty compact Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
min_dist_min (P1,C1) is V11() V12() ext-real Element of REAL
C ` is V21() Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ C is set
(min_dist_min (P1,C1)) / 2 is V11() V12() ext-real Element of REAL
n is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Gauge (C,n) is V13() V15() V16( NAT ) V17(K324( the carrier of (TOP-REAL 2))) V18() V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K324( the carrier of (TOP-REAL 2))
(Gauge (C,n)) * (1,1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * (1,2) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) is V11() V12() ext-real Element of REAL
(Gauge (C,n)) * (2,1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) is V11() V12() ext-real Element of REAL
Cage (C,n) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,n)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
UBD (L~ (Cage (C,n))) is non empty V21() open connected being_Region Element of K6( the carrier of (TOP-REAL 2))
(L~ (Cage (C,n))) /\ P is V21() Element of K6( the carrier of (TOP-REAL 2))
a is set
len (Cage (C,n)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
i is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
i + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
LSeg ((Cage (C,n)),i) is V21() Element of K6( the carrier of (TOP-REAL 2))
right_cell ((Cage (C,n)),i,(Gauge (C,n))) is V21() Element of K6( the carrier of (TOP-REAL 2))
(right_cell ((Cage (C,n)),i,(Gauge (C,n)))) /\ C is V21() Element of K6( the carrier of (TOP-REAL 2))
c is set
the carrier of (Euclid 2) is non empty set
c is Element of the carrier of (Euclid 2)
Indices (Gauge (C,n)) is set
(Cage (C,n)) /. i is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Cage (C,n)) /. (i + 1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
i1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
j1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
[i1,j1] is set
{i1,j1} is non empty V150() V151() V152() V153() V154() V155() set
{i1} is non empty V150() V151() V152() V153() V154() V155() set
{{i1,j1},{i1}} is non empty set
(Gauge (C,n)) * (i1,j1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
i2 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
j2 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
[i2,j2] is set
{i2,j2} is non empty V150() V151() V152() V153() V154() V155() set
{i2} is non empty V150() V151() V152() V153() V154() V155() set
{{i2,j2},{i2}} is non empty set
(Gauge (C,n)) * (i2,j2) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
j1 + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
i1 + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
i2 + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
j2 + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
left_cell ((Cage (C,n)),i,(Gauge (C,n))) is V21() Element of K6( the carrier of (TOP-REAL 2))
(left_cell ((Cage (C,n)),i,(Gauge (C,n)))) /\ (right_cell ((Cage (C,n)),i,(Gauge (C,n)))) is V21() Element of K6( the carrier of (TOP-REAL 2))
a9 is Element of the carrier of (Euclid 2)
dist (a9,c) is V11() V12() ext-real Element of REAL
E-bound C is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | C is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 | C is V13() V16( the carrier of ((TOP-REAL 2) | C)) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | C), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))
the carrier of ((TOP-REAL 2) | C) is non empty set
K7( the carrier of ((TOP-REAL 2) | C),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | C),REAL)) is non empty set
K360(((TOP-REAL 2) | C),(proj1 | C)) is V11() V12() ext-real Element of REAL
W-bound C is V11() V12() ext-real Element of REAL
K359(((TOP-REAL 2) | C),(proj1 | C)) is V11() V12() ext-real Element of REAL
N-bound C is V11() V12() ext-real Element of REAL
proj2 | C is V13() V16( the carrier of ((TOP-REAL 2) | C)) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | C), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))
K360(((TOP-REAL 2) | C),(proj2 | C)) is V11() V12() ext-real Element of REAL
S-bound C is V11() V12() ext-real Element of REAL
K359(((TOP-REAL 2) | C),(proj2 | C)) is V11() V12() ext-real Element of REAL
len (Gauge (C,n)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
width (Gauge (C,n)) is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
[1,1] is set
{1,1} is non empty V150() V151() V152() V153() V154() V155() set
{1} is non empty V150() V151() V152() V153() V154() V155() set
{{1,1},{1}} is non empty set
[(i1 + 1),1] is set
{(i1 + 1),1} is non empty V150() V151() V152() V153() V154() V155() set
{(i1 + 1)} is non empty V150() V151() V152() V153() V154() V155() set
{{(i1 + 1),1},{(i1 + 1)}} is non empty set
[i1,1] is set
{i1,1} is non empty V150() V151() V152() V153() V154() V155() set
{{i1,1},{i1}} is non empty set
(Gauge (C,n)) * (i1,1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * ((i1 + 1),1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,n)) * (i1,1)),((Gauge (C,n)) * ((i1 + 1),1))) is V11() V12() ext-real Element of REAL
((Gauge (C,n)) * ((i1 + 1),1)) `1 is V11() V12() ext-real Element of REAL
((Gauge (C,n)) * (i1,1)) `1 is V11() V12() ext-real Element of REAL
(((Gauge (C,n)) * ((i1 + 1),1)) `1) - (((Gauge (C,n)) * (i1,1)) `1) is V11() V12() ext-real Element of REAL
(E-bound C) - (W-bound C) is V11() V12() ext-real Element of REAL
2 |^ n is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
((E-bound C) - (W-bound C)) / (2 |^ n) is V11() V12() ext-real Element of REAL
[1,(j1 + 1)] is set
{1,(j1 + 1)} is non empty V150() V151() V152() V153() V154() V155() set
{{1,(j1 + 1)},{1}} is non empty set
cell ((Gauge (C,n)),i1,j1) is V21() Element of K6( the carrier of (TOP-REAL 2))
(Gauge (C,n)) * (1,j1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * (1,j1)) `2 is V11() V12() ext-real Element of REAL
(Gauge (C,n)) * (1,(j1 + 1)) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * (1,(j1 + 1))) `2 is V11() V12() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() V12() ext-real Element of REAL : ( ((Gauge (C,n)) * (i1,1)) `1 <= b1 & b1 <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= b2 & b2 <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) } is set
aa is V11() V12() ext-real Element of REAL
ab is V11() V12() ext-real Element of REAL
|[aa,ab]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
A is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
A `1 is V11() V12() ext-real Element of REAL
A `2 is V11() V12() ext-real Element of REAL
[1,j1] is set
{1,j1} is non empty V150() V151() V152() V153() V154() V155() set
{{1,j1},{1}} is non empty set
dist (((Gauge (C,n)) * (1,j1)),((Gauge (C,n)) * (1,(j1 + 1)))) is V11() V12() ext-real Element of REAL
(((Gauge (C,n)) * (1,(j1 + 1))) `2) - (((Gauge (C,n)) * (1,j1)) `2) is V11() V12() ext-real Element of REAL
(N-bound C) - (S-bound C) is V11() V12() ext-real Element of REAL
((N-bound C) - (S-bound C)) / (2 |^ n) is V11() V12() ext-real Element of REAL
r is V11() V12() ext-real Element of REAL
t is V11() V12() ext-real Element of REAL
|[r,t]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
c9 is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
c9 `1 is V11() V12() ext-real Element of REAL
c9 `2 is V11() V12() ext-real Element of REAL
dist (A,c9) is V11() V12() ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) is V11() V12() ext-real Element of REAL
[(i1 + 1),1] is set
{(i1 + 1),1} is non empty V150() V151() V152() V153() V154() V155() set
{(i1 + 1)} is non empty V150() V151() V152() V153() V154() V155() set
{{(i1 + 1),1},{(i1 + 1)}} is non empty set
[i1,1] is set
{i1,1} is non empty V150() V151() V152() V153() V154() V155() set
{{i1,1},{i1}} is non empty set
(Gauge (C,n)) * (i1,1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * ((i1 + 1),1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,n)) * (i1,1)),((Gauge (C,n)) * ((i1 + 1),1))) is V11() V12() ext-real Element of REAL
((Gauge (C,n)) * ((i1 + 1),1)) `1 is V11() V12() ext-real Element of REAL
((Gauge (C,n)) * (i1,1)) `1 is V11() V12() ext-real Element of REAL
(((Gauge (C,n)) * ((i1 + 1),1)) `1) - (((Gauge (C,n)) * (i1,1)) `1) is V11() V12() ext-real Element of REAL
(E-bound C) - (W-bound C) is V11() V12() ext-real Element of REAL
2 |^ n is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
((E-bound C) - (W-bound C)) / (2 |^ n) is V11() V12() ext-real Element of REAL
j2 - 1 is V11() V12() ext-real Element of REAL
j2 -' 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
(width (Gauge (C,n))) - 0 is V11() V12() ext-real Element of REAL
(width (Gauge (C,n))) - 1 is V11() V12() ext-real Element of REAL
[1,(j2 -' 1)] is set
{1,(j2 -' 1)} is non empty V150() V151() V152() V153() V154() V155() set
{{1,(j2 -' 1)},{1}} is non empty set
cell ((Gauge (C,n)),i1,(j2 -' 1)) is V21() Element of K6( the carrier of (TOP-REAL 2))
(Gauge (C,n)) * (1,(j2 -' 1)) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * (1,(j2 -' 1))) `2 is V11() V12() ext-real Element of REAL
(j2 -' 1) + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
(Gauge (C,n)) * (1,((j2 -' 1) + 1)) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * (1,((j2 -' 1) + 1))) `2 is V11() V12() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() V12() ext-real Element of REAL : ( ((Gauge (C,n)) * (i1,1)) `1 <= b1 & b1 <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,(j2 -' 1))) `2 <= b2 & b2 <= ((Gauge (C,n)) * (1,((j2 -' 1) + 1))) `2 ) } is set
aa is V11() V12() ext-real Element of REAL
ab is V11() V12() ext-real Element of REAL
|[aa,ab]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
A is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
A `1 is V11() V12() ext-real Element of REAL
A `2 is V11() V12() ext-real Element of REAL
[1,((j2 -' 1) + 1)] is set
{1,((j2 -' 1) + 1)} is non empty V150() V151() V152() V153() V154() V155() set
{{1,((j2 -' 1) + 1)},{1}} is non empty set
dist (((Gauge (C,n)) * (1,(j2 -' 1))),((Gauge (C,n)) * (1,((j2 -' 1) + 1)))) is V11() V12() ext-real Element of REAL
(((Gauge (C,n)) * (1,((j2 -' 1) + 1))) `2) - (((Gauge (C,n)) * (1,(j2 -' 1))) `2) is V11() V12() ext-real Element of REAL
(N-bound C) - (S-bound C) is V11() V12() ext-real Element of REAL
((N-bound C) - (S-bound C)) / (2 |^ n) is V11() V12() ext-real Element of REAL
r is V11() V12() ext-real Element of REAL
t is V11() V12() ext-real Element of REAL
|[r,t]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
c9 is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
c9 `1 is V11() V12() ext-real Element of REAL
c9 `2 is V11() V12() ext-real Element of REAL
dist (A,c9) is V11() V12() ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) is V11() V12() ext-real Element of REAL
[1,(j1 + 1)] is set
{1,(j1 + 1)} is non empty V150() V151() V152() V153() V154() V155() set
{{1,(j1 + 1)},{1}} is non empty set
[1,j1] is set
{1,j1} is non empty V150() V151() V152() V153() V154() V155() set
{{1,j1},{1}} is non empty set
(Gauge (C,n)) * (1,j1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * (1,(j1 + 1)) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,n)) * (1,j1)),((Gauge (C,n)) * (1,(j1 + 1)))) is V11() V12() ext-real Element of REAL
((Gauge (C,n)) * (1,(j1 + 1))) `2 is V11() V12() ext-real Element of REAL
((Gauge (C,n)) * (1,j1)) `2 is V11() V12() ext-real Element of REAL
(((Gauge (C,n)) * (1,(j1 + 1))) `2) - (((Gauge (C,n)) * (1,j1)) `2) is V11() V12() ext-real Element of REAL
(N-bound C) - (S-bound C) is V11() V12() ext-real Element of REAL
2 |^ n is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
((N-bound C) - (S-bound C)) / (2 |^ n) is V11() V12() ext-real Element of REAL
[(i2 + 1),1] is set
{(i2 + 1),1} is non empty V150() V151() V152() V153() V154() V155() set
{(i2 + 1)} is non empty V150() V151() V152() V153() V154() V155() set
{{(i2 + 1),1},{(i2 + 1)}} is non empty set
cell ((Gauge (C,n)),i2,j1) is V21() Element of K6( the carrier of (TOP-REAL 2))
(Gauge (C,n)) * (i2,1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * (i2,1)) `1 is V11() V12() ext-real Element of REAL
(Gauge (C,n)) * ((i2 + 1),1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * ((i2 + 1),1)) `1 is V11() V12() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() V12() ext-real Element of REAL : ( ((Gauge (C,n)) * (i2,1)) `1 <= b1 & b1 <= ((Gauge (C,n)) * ((i2 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= b2 & b2 <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) } is set
aa is V11() V12() ext-real Element of REAL
ab is V11() V12() ext-real Element of REAL
|[aa,ab]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
A is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
A `1 is V11() V12() ext-real Element of REAL
A `2 is V11() V12() ext-real Element of REAL
[i2,1] is set
{i2,1} is non empty V150() V151() V152() V153() V154() V155() set
{{i2,1},{i2}} is non empty set
dist (((Gauge (C,n)) * (i2,1)),((Gauge (C,n)) * ((i2 + 1),1))) is V11() V12() ext-real Element of REAL
(((Gauge (C,n)) * ((i2 + 1),1)) `1) - (((Gauge (C,n)) * (i2,1)) `1) is V11() V12() ext-real Element of REAL
(E-bound C) - (W-bound C) is V11() V12() ext-real Element of REAL
((E-bound C) - (W-bound C)) / (2 |^ n) is V11() V12() ext-real Element of REAL
r is V11() V12() ext-real Element of REAL
t is V11() V12() ext-real Element of REAL
|[r,t]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
c9 is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
c9 `1 is V11() V12() ext-real Element of REAL
c9 `2 is V11() V12() ext-real Element of REAL
dist (A,c9) is V11() V12() ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) is V11() V12() ext-real Element of REAL
[1,(j2 + 1)] is set
{1,(j2 + 1)} is non empty V150() V151() V152() V153() V154() V155() set
{{1,(j2 + 1)},{1}} is non empty set
[1,j2] is set
{1,j2} is non empty V150() V151() V152() V153() V154() V155() set
{{1,j2},{1}} is non empty set
(Gauge (C,n)) * (1,j2) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * (1,(j2 + 1)) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,n)) * (1,j2)),((Gauge (C,n)) * (1,(j2 + 1)))) is V11() V12() ext-real Element of REAL
((Gauge (C,n)) * (1,(j2 + 1))) `2 is V11() V12() ext-real Element of REAL
((Gauge (C,n)) * (1,j2)) `2 is V11() V12() ext-real Element of REAL
(((Gauge (C,n)) * (1,(j2 + 1))) `2) - (((Gauge (C,n)) * (1,j2)) `2) is V11() V12() ext-real Element of REAL
(N-bound C) - (S-bound C) is V11() V12() ext-real Element of REAL
2 |^ n is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
((N-bound C) - (S-bound C)) / (2 |^ n) is V11() V12() ext-real Element of REAL
i1 - 1 is V11() V12() ext-real Element of REAL
i1 -' 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
(len (Gauge (C,n))) - 0 is V11() V12() ext-real Element of REAL
(len (Gauge (C,n))) - 1 is V11() V12() ext-real Element of REAL
[(i1 -' 1),1] is set
{(i1 -' 1),1} is non empty V150() V151() V152() V153() V154() V155() set
{(i1 -' 1)} is non empty V150() V151() V152() V153() V154() V155() set
{{(i1 -' 1),1},{(i1 -' 1)}} is non empty set
cell ((Gauge (C,n)),(i1 -' 1),j2) is V21() Element of K6( the carrier of (TOP-REAL 2))
(Gauge (C,n)) * ((i1 -' 1),1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * ((i1 -' 1),1)) `1 is V11() V12() ext-real Element of REAL
(i1 -' 1) + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
(Gauge (C,n)) * (((i1 -' 1) + 1),1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * (((i1 -' 1) + 1),1)) `1 is V11() V12() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() V12() ext-real Element of REAL : ( ((Gauge (C,n)) * ((i1 -' 1),1)) `1 <= b1 & b1 <= ((Gauge (C,n)) * (((i1 -' 1) + 1),1)) `1 & ((Gauge (C,n)) * (1,j2)) `2 <= b2 & b2 <= ((Gauge (C,n)) * (1,(j2 + 1))) `2 ) } is set
aa is V11() V12() ext-real Element of REAL
ab is V11() V12() ext-real Element of REAL
|[aa,ab]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
A is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
A `1 is V11() V12() ext-real Element of REAL
A `2 is V11() V12() ext-real Element of REAL
[((i1 -' 1) + 1),1] is set
{((i1 -' 1) + 1),1} is non empty V150() V151() V152() V153() V154() V155() set
{((i1 -' 1) + 1)} is non empty V150() V151() V152() V153() V154() V155() set
{{((i1 -' 1) + 1),1},{((i1 -' 1) + 1)}} is non empty set
dist (((Gauge (C,n)) * ((i1 -' 1),1)),((Gauge (C,n)) * (((i1 -' 1) + 1),1))) is V11() V12() ext-real Element of REAL
(((Gauge (C,n)) * (((i1 -' 1) + 1),1)) `1) - (((Gauge (C,n)) * ((i1 -' 1),1)) `1) is V11() V12() ext-real Element of REAL
(E-bound C) - (W-bound C) is V11() V12() ext-real Element of REAL
((E-bound C) - (W-bound C)) / (2 |^ n) is V11() V12() ext-real Element of REAL
r is V11() V12() ext-real Element of REAL
t is V11() V12() ext-real Element of REAL
|[r,t]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
c9 is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
c9 `1 is V11() V12() ext-real Element of REAL
c9 `2 is V11() V12() ext-real Element of REAL
dist (A,c9) is V11() V12() ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) is V11() V12() ext-real Element of REAL
A is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
c9 is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
dist (A,c9) is V11() V12() ext-real Element of REAL
(N-bound C) - (S-bound C) is V11() V12() ext-real Element of REAL
2 |^ n is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
((N-bound C) - (S-bound C)) / (2 |^ n) is V11() V12() ext-real Element of REAL
(E-bound C) - (W-bound C) is V11() V12() ext-real Element of REAL
((E-bound C) - (W-bound C)) / (2 |^ n) is V11() V12() ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) is V11() V12() ext-real Element of REAL
A is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
c9 is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
dist (A,c9) is V11() V12() ext-real Element of REAL
(N-bound C) - (S-bound C) is V11() V12() ext-real Element of REAL
2 |^ n is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
((N-bound C) - (S-bound C)) / (2 |^ n) is V11() V12() ext-real Element of REAL
(E-bound C) - (W-bound C) is V11() V12() ext-real Element of REAL
((E-bound C) - (W-bound C)) / (2 |^ n) is V11() V12() ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) is V11() V12() ext-real Element of REAL
1 + 1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
[(1 + 1),1] is set
{(1 + 1),1} is non empty V150() V151() V152() V153() V154() V155() set
{(1 + 1)} is non empty V150() V151() V152() V153() V154() V155() set
{{(1 + 1),1},{(1 + 1)}} is non empty set
(Gauge (C,n)) * ((1 + 1),1) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * ((1 + 1),1))) is V11() V12() ext-real Element of REAL
[1,(1 + 1)] is set
{1,(1 + 1)} is non empty V150() V151() V152() V153() V154() V155() set
{{1,(1 + 1)},{1}} is non empty set
(Gauge (C,n)) * (1,(1 + 1)) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,(1 + 1)))) is V11() V12() ext-real Element of REAL
((min_dist_min (P1,C1)) / 2) + ((min_dist_min (P1,C1)) / 2) is V11() V12() ext-real Element of REAL
(L~ (Cage (C,n))) ` is V21() Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ (Cage (C,n))) is set
a is set
N-bound (L~ (Cage (C,n))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (C,n))) is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj2 | (L~ (Cage (C,n))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,n))))) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,n)))), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,n)))),REAL))
the carrier of ((TOP-REAL 2) | (L~ (Cage (C,n)))) is non empty set
K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,n)))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,n)))),REAL)) is non empty set
K360(((TOP-REAL 2) | (L~ (Cage (C,n)))),(proj2 | (L~ (Cage (C,n))))) is V11() V12() ext-real Element of REAL
(Cage (C,n)) /. 1 is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
N-min (L~ (Cage (C,n))) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
N-most (L~ (Cage (C,n))) is V21() Element of K6( the carrier of (TOP-REAL 2))
NW-corner (L~ (Cage (C,n))) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
W-bound (L~ (Cage (C,n))) is V11() V12() ext-real Element of REAL
proj1 | (L~ (Cage (C,n))) is V13() V16( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,n))))) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,n)))), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (C,n)))),REAL))
K359(((TOP-REAL 2) | (L~ (Cage (C,n)))),(proj1 | (L~ (Cage (C,n))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (C,n)))),(N-bound (L~ (Cage (C,n))))]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
NE-corner (L~ (Cage (C,n))) is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
E-bound (L~ (Cage (C,n))) is V11() V12() ext-real Element of REAL
K360(((TOP-REAL 2) | (L~ (Cage (C,n)))),(proj1 | (L~ (Cage (C,n))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (C,n)))),(N-bound (L~ (Cage (C,n))))]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
LSeg ((NW-corner (L~ (Cage (C,n)))),(NE-corner (L~ (Cage (C,n))))) is V21() closed closed boundary connected bounded bounded compact compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((NW-corner (L~ (Cage (C,n)))),(NE-corner (L~ (Cage (C,n)))))) /\ (L~ (Cage (C,n))) is V21() Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (N-most (L~ (Cage (C,n)))) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 | (N-most (L~ (Cage (C,n)))) is V13() V16( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (C,n)))))) V17( REAL ) V18() V40( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (C,n))))), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (C,n))))),REAL))
the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (C,n))))) is set
K7( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (C,n))))),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (N-most (L~ (Cage (C,n))))),REAL)) is non empty set
K359(((TOP-REAL 2) | (N-most (L~ (Cage (C,n))))),(proj1 | (N-most (L~ (Cage (C,n)))))) is V11() V12() ext-real Element of REAL
|[K359(((TOP-REAL 2) | (N-most (L~ (Cage (C,n))))),(proj1 | (N-most (L~ (Cage (C,n)))))),(N-bound (L~ (Cage (C,n))))]| is non empty V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
LeftComp (Cage (C,n)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
{B} is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
a is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
a is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
(TOP-REAL 2) | ((L~ (Cage (C,n))) `) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) is set
K6( the carrier of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `))) is non empty set
K6( the carrier of (Euclid 2)) is non empty set
a is Element of K6( the carrier of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)))
C is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
(C) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))
{ (Cl (BDD (L~ (Cage (C,b1))))) where b1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT : verum } is set
meet (C) is V21() Element of K6( the carrier of (TOP-REAL 2))
x is set
Y is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Cage (C,Y) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,Y)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Cage (C,Y))) is V21() open Element of K6( the carrier of (TOP-REAL 2))
Cl (BDD (L~ (Cage (C,Y)))) is V21() Element of K6( the carrier of (TOP-REAL 2))
C is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
x is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
BDD x is V21() open Element of K6( the carrier of (TOP-REAL 2))
Cage (x,C) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
LeftComp (Cage (x,C)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
(BDD x) /\ (LeftComp (Cage (x,C))) is V21() Element of K6( the carrier of (TOP-REAL 2))
n is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
UBD x is non empty V21() open connected being_Region Element of K6( the carrier of (TOP-REAL 2))
(BDD x) /\ (UBD x) is V21() Element of K6( the carrier of (TOP-REAL 2))
(x) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))
{ (UBD (L~ (Cage (x,b1)))) where b1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT : verum } is set
union (x) is V21() Element of K6( the carrier of (TOP-REAL 2))
L~ (Cage (x,C)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
UBD (L~ (Cage (x,C))) is non empty V21() open connected being_Region Element of K6( the carrier of (TOP-REAL 2))
C is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
x is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
BDD x is V21() open Element of K6( the carrier of (TOP-REAL 2))
Cage (x,C) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
RightComp (Cage (x,C)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
n is set
L~ (Cage (x,C)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
LeftComp (Cage (x,C)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
UBD (L~ (Cage (x,C))) is non empty V21() open connected being_Region Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V21() Element of K6( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of L~ (Cage (x,C)) } is set
union { b1 where b1 is V21() Element of K6( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of L~ (Cage (x,C)) } is set
Cl (LeftComp (Cage (x,C))) is V21() Element of K6( the carrier of (TOP-REAL 2))
UBD x is non empty V21() open connected being_Region Element of K6( the carrier of (TOP-REAL 2))
(BDD x) /\ (UBD x) is V21() Element of K6( the carrier of (TOP-REAL 2))
(x) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))
{ (UBD (L~ (Cage (x,b1)))) where b1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT : verum } is set
union (x) is V21() Element of K6( the carrier of (TOP-REAL 2))
(Cl (LeftComp (Cage (x,C)))) \ (LeftComp (Cage (x,C))) is V21() Element of K6( the carrier of (TOP-REAL 2))
C is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
x is V21() Element of K6( the carrier of (TOP-REAL 2))
Y is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Cage (Y,C) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (Y,C)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
BDD Y is V21() open Element of K6( the carrier of (TOP-REAL 2))
x /\ (L~ (Cage (Y,C))) is V21() Element of K6( the carrier of (TOP-REAL 2))
B is V13() V16( NAT ) V18() V28() V35(2) FinSequence-like FinSubsequence-like V142() Element of the carrier of (TOP-REAL 2)
RightComp (Cage (Y,C)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
C is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
x is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
BDD x is V21() open Element of K6( the carrier of (TOP-REAL 2))
Cage (x,C) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (x,C)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
(BDD x) /\ (L~ (Cage (x,C))) is V21() Element of K6( the carrier of (TOP-REAL 2))
Y is set
{ b1 where b1 is V21() Element of K6( the carrier of (TOP-REAL 2)) : b1 is_inside_component_of x } is set
union { b1 where b1 is V21() Element of K6( the carrier of (TOP-REAL 2)) : b1 is_inside_component_of x } is set
n is set
B is V21() Element of K6( the carrier of (TOP-REAL 2))
B /\ (L~ (Cage (x,C))) is V21() Element of K6( the carrier of (TOP-REAL 2))
C is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
(C) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))
{ (UBD (L~ (Cage (C,b1)))) where b1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT : verum } is set
COMPLEMENT (C) is Element of K6(K6( the carrier of (TOP-REAL 2)))
(C) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))
{ (Cl (BDD (L~ (Cage (C,b1))))) where b1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT : verum } is set
x is V21() Element of K6( the carrier of (TOP-REAL 2))
x ` is V21() Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ x is set
Y is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Cage (C,Y) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,Y)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Cage (C,Y))) is V21() open Element of K6( the carrier of (TOP-REAL 2))
Cl (BDD (L~ (Cage (C,Y)))) is V21() Element of K6( the carrier of (TOP-REAL 2))
RightComp (Cage (C,Y)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
Cl (RightComp (Cage (C,Y))) is V21() closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
(RightComp (Cage (C,Y))) \/ (L~ (Cage (C,Y))) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
LeftComp (Cage (C,Y)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
(LeftComp (Cage (C,Y))) ` is V21() Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (LeftComp (Cage (C,Y))) is set
(x `) /\ ((LeftComp (Cage (C,Y))) `) is V21() Element of K6( the carrier of (TOP-REAL 2))
x \/ (LeftComp (Cage (C,Y))) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
(x \/ (LeftComp (Cage (C,Y)))) ` is V21() Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (x \/ (LeftComp (Cage (C,Y)))) is set
[#] the carrier of (TOP-REAL 2) is non empty non proper V21() Element of K6( the carrier of (TOP-REAL 2))
([#] the carrier of (TOP-REAL 2)) ` is V21() Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ ([#] the carrier of (TOP-REAL 2)) is set
{} the carrier of (TOP-REAL 2) is empty proper V18() V21() FinSequence-membered closed connected V150() V151() V152() V153() V154() V155() V156() bounded compact horizontal vertical Element of K6( the carrier of (TOP-REAL 2))
UBD (L~ (Cage (C,Y))) is non empty V21() open connected being_Region Element of K6( the carrier of (TOP-REAL 2))
Y is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Cage (C,Y) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,Y)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
UBD (L~ (Cage (C,Y))) is non empty V21() open connected being_Region Element of K6( the carrier of (TOP-REAL 2))
LeftComp (Cage (C,Y)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
RightComp (Cage (C,Y)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
(RightComp (Cage (C,Y))) \/ (L~ (Cage (C,Y))) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
Cl (RightComp (Cage (C,Y))) is V21() closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
(x `) ` is V21() Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (x `) is set
(Cl (RightComp (Cage (C,Y)))) ` is V21() Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (Cl (RightComp (Cage (C,Y)))) is set
((x `) `) /\ ((Cl (RightComp (Cage (C,Y)))) `) is V21() Element of K6( the carrier of (TOP-REAL 2))
(x `) \/ (Cl (RightComp (Cage (C,Y)))) is V21() Element of K6( the carrier of (TOP-REAL 2))
((x `) \/ (Cl (RightComp (Cage (C,Y))))) ` is V21() Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ ((x `) \/ (Cl (RightComp (Cage (C,Y))))) is set
(x `) \/ ((RightComp (Cage (C,Y))) \/ (L~ (Cage (C,Y)))) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
((x `) \/ ((RightComp (Cage (C,Y))) \/ (L~ (Cage (C,Y))))) ` is V21() Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ ((x `) \/ ((RightComp (Cage (C,Y))) \/ (L~ (Cage (C,Y))))) is set
[#] the carrier of (TOP-REAL 2) is non empty non proper V21() Element of K6( the carrier of (TOP-REAL 2))
([#] the carrier of (TOP-REAL 2)) ` is V21() Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ ([#] the carrier of (TOP-REAL 2)) is set
{} the carrier of (TOP-REAL 2) is empty proper V18() V21() FinSequence-membered closed connected V150() V151() V152() V153() V154() V155() V156() bounded compact horizontal vertical Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Cage (C,Y))) is V21() open Element of K6( the carrier of (TOP-REAL 2))
Cl (BDD (L~ (Cage (C,Y)))) is V21() Element of K6( the carrier of (TOP-REAL 2))
C is non empty V21() closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
(C) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))
{ (Cl (BDD (L~ (Cage (C,b1))))) where b1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT : verum } is set
meet (C) is V21() Element of K6( the carrier of (TOP-REAL 2))
BDD C is V21() open Element of K6( the carrier of (TOP-REAL 2))
C \/ (BDD C) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
x is set
(C) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))
{ (UBD (L~ (Cage (C,b1)))) where b1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT : verum } is set
COMPLEMENT (C) is Element of K6(K6( the carrier of (TOP-REAL 2)))
[#] the carrier of (TOP-REAL 2) is non empty non proper V21() Element of K6( the carrier of (TOP-REAL 2))
union (C) is V21() Element of K6( the carrier of (TOP-REAL 2))
([#] the carrier of (TOP-REAL 2)) \ (union (C)) is V21() Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty V21() open connected being_Region Element of K6( the carrier of (TOP-REAL 2))
(BDD C) \/ (UBD C) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
C ` is V21() Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ C is set
UBD C is non empty V21() open connected being_Region Element of K6( the carrier of (TOP-REAL 2))
(BDD C) /\ (UBD C) is V21() Element of K6( the carrier of (TOP-REAL 2))
x is set
(C) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))
{ (UBD (L~ (Cage (C,b1)))) where b1 is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT : verum } is set
union (C) is V21() Element of K6( the carrier of (TOP-REAL 2))
Y is set
n is V10() V11() V12() V26() ext-real V103() V150() V151() V152() V153() V154() V155() Element of NAT
Cage (C,n) is non empty non trivial V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V20() V28() FinSequence-like FinSubsequence-like V208( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V226() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,n)) is non empty V21() closed boundary bounded compact Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Cage (C,n))) is V21() open Element of K6( the carrier of (TOP-REAL 2))
Cl (BDD (L~ (Cage (C,n)))) is V21() Element of K6( the carrier of (TOP-REAL 2))
LeftComp (Cage (C,n)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V21() Element of K6( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of L~ (Cage (C,n)) } is set
(BDD C) /\ (L~ (Cage (C,n))) is V21() Element of K6( the carrier of (TOP-REAL 2))
RightComp (Cage (C,n)) is non empty V21() Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V21() Element of K6( the carrier of (TOP-REAL 2)) : b1 is_inside_component_of L~ (Cage (C,n)) } is set
UBD (L~ (Cage (C,n))) is non empty V21() open connected being_Region Element of K6( the carrier of (TOP-REAL 2))
union { b1 where b1 is V21() Element of K6( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of L~ (Cage (C,n)) } is set
union { b1 where b1 is V21() Element of K6( the carrier of (TOP-REAL 2)) : b1 is_inside_component_of L~ (Cage (C,n)) } is set