:: JORDAN10 semantic presentation

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)),b

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

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

{ |[b

{ |[b

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

{ b

union { b

n is set

{ b

union { b

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,b

{ (Cl (BDD (L~ (Cage (C,b

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,b

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,b

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,b

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