:: JORDAN19 semantic presentation

REAL is set

NAT is non empty epsilon-transitive epsilon-connected ordinal V28() V33() V34() Element of K6(REAL)

K6(REAL) is non empty set

COMPLEX is set

omega is non empty epsilon-transitive epsilon-connected ordinal V28() V33() V34() set

K6(omega) is non empty V28() set

K6(NAT) is non empty V28() set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

K7(2,2) is non empty set

K7(K7(2,2),2) is non empty set

K6(K7(K7(2,2),2)) is non empty set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

RAT is set

INT is set

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

K7(K7(2,2),REAL) is set

K6(K7(K7(2,2),REAL)) is non empty set

K6(K7(REAL,REAL)) is non empty set

TOP-REAL 2 is non empty non trivial TopSpace-like T_2 V85() V110() V111() V112() V113() V114() V115() V116() strict add-continuous Mult-continuous RLTopStruct

the carrier of (TOP-REAL 2) is non empty non trivial functional set

K307( the carrier of (TOP-REAL 2)) is non empty functional FinSequence-membered M16( the carrier of (TOP-REAL 2))

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

K7(COMPLEX,COMPLEX) is set

K6(K7(COMPLEX,COMPLEX)) is non empty set

K7(COMPLEX,REAL) is set

K6(K7(COMPLEX,REAL)) is non empty set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Function-like functional V28() V33() V35( {} ) FinSequence-membered ext-real non positive non negative set

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Function-like functional V28() V33() V35( {} ) FinSequence-membered ext-real non positive non negative set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Function-like functional V28() V33() V35( {} ) FinSequence-membered ext-real non positive non negative set

3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

K7(NAT, the carrier of (TOP-REAL 2)) is non empty V28() set

Seg 1 is non empty trivial V28() V35(1) Element of K6(NAT)

{1} is non empty trivial V35(1) set

Seg 2 is non empty V28() V35(2) Element of K6(NAT)

{1,2} is non empty set

Seg 3 is non empty V28() V35(3) Element of K6(NAT)

{1,2,3} is non empty set

4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

proj1 is V15() V18( the carrier of (TOP-REAL 2)) V19( REAL ) Function-like V40( the carrier of (TOP-REAL 2), REAL ) V212( TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))

proj2 is V15() V18( the carrier of (TOP-REAL 2)) V19( REAL ) Function-like V40( the carrier of (TOP-REAL 2), REAL ) V212( TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Function-like functional V28() V33() V35( {} ) FinSequence-membered ext-real non positive non negative Element of NAT

K291( the carrier of (TOP-REAL 2)) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))

K6(K6( the carrier of (TOP-REAL 2))) is non empty set

K7(NAT,K291( the carrier of (TOP-REAL 2))) is non empty V28() set

K6(K7(NAT,K291( the carrier of (TOP-REAL 2)))) is non empty V28() set

C is non empty functional closed connected bounded being_simple_closed_curve compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))

C is non empty functional closed connected bounded being_simple_closed_curve compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))

(C) is V15() V18( NAT ) V19(K291( the carrier of (TOP-REAL 2))) Function-like V40( NAT ,K291( the carrier of (TOP-REAL 2))) Element of K6(K7(NAT,K291( the carrier of (TOP-REAL 2))))

Lim_inf (C) is functional Element of K6( the carrier of (TOP-REAL 2))

(C) is V15() V18( NAT ) V19(K291( the carrier of (TOP-REAL 2))) Function-like V40( NAT ,K291( the carrier of (TOP-REAL 2))) Element of K6(K7(NAT,K291( the carrier of (TOP-REAL 2))))

Lim_inf (C) is functional Element of K6( the carrier of (TOP-REAL 2))

p is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

C is V15() non empty-yielding V18( NAT ) V19(K307( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K307( the carrier of (TOP-REAL 2))

width C is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

len C is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

(len C) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

((len C) div 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

Center C is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

[(Center C),p] is set

{(Center C),p} is non empty set

{(Center C)} is non empty trivial V35(1) set

{{(Center C),p},{(Center C)}} is non empty set

Indices C is set

C is non empty functional Element of K6( the carrier of (TOP-REAL 2))

N-bound C is V11() real ext-real Element of REAL

(TOP-REAL 2) | C is strict T_2 SubSpace of TOP-REAL 2

proj2 | C is V15() V18( the carrier of ((TOP-REAL 2) | C)) V19( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | C), REAL ) V212((TOP-REAL 2) | C) Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

the carrier of ((TOP-REAL 2) | C) is set

K7( the carrier of ((TOP-REAL 2) | C),REAL) is set

K6(K7( the carrier of ((TOP-REAL 2) | C),REAL)) is non empty set

upper_bound (proj2 | C) is V11() real ext-real Element of REAL

(proj2 | C) .: the carrier of ((TOP-REAL 2) | C) is Element of K6(REAL)

upper_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

S-bound C is V11() real ext-real Element of REAL

lower_bound (proj2 | C) is V11() real ext-real Element of REAL

lower_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

W-bound C is V11() real ext-real Element of REAL

proj1 | C is V15() V18( the carrier of ((TOP-REAL 2) | C)) V19( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | C), REAL ) V212((TOP-REAL 2) | C) Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

lower_bound (proj1 | C) is V11() real ext-real Element of REAL

(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is Element of K6(REAL)

lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

E-bound C is V11() real ext-real Element of REAL

upper_bound (proj1 | C) is V11() real ext-real Element of REAL

upper_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

p is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

Gauge (C,p) is V15() non empty-yielding V18( NAT ) V19(K307( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K307( the carrier of (TOP-REAL 2))

p9 is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

width (Gauge (C,p)) is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

[p9,(width (Gauge (C,p)))] is set

{p9,(width (Gauge (C,p)))} is non empty set

{p9} is non empty trivial V35(1) set

{{p9,(width (Gauge (C,p)))},{p9}} is non empty set

Indices (Gauge (C,p)) is set

(Gauge (C,p)) * (p9,(width (Gauge (C,p)))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

((Gauge (C,p)) * (p9,(width (Gauge (C,p))))) `2 is V11() real ext-real Element of REAL

(E-bound C) - (W-bound C) is V11() real ext-real Element of REAL

- (W-bound C) is V11() real ext-real set

(E-bound C) + (- (W-bound C)) is V11() real ext-real set

2 |^ p is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

((E-bound C) - (W-bound C)) / (2 |^ p) is V11() real ext-real Element of REAL

(2 |^ p) " is V11() real ext-real non negative set

((E-bound C) - (W-bound C)) * ((2 |^ p) ") is V11() real ext-real set

p9 - 2 is V11() real ext-real Element of REAL

- 2 is V11() real ext-real non positive set

p9 + (- 2) is V11() real ext-real set

(((E-bound C) - (W-bound C)) / (2 |^ p)) * (p9 - 2) is V11() real ext-real Element of REAL

(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ p)) * (p9 - 2)) is V11() real ext-real Element of REAL

(N-bound C) - (S-bound C) is V11() real ext-real Element of REAL

- (S-bound C) is V11() real ext-real set

(N-bound C) + (- (S-bound C)) is V11() real ext-real set

((N-bound C) - (S-bound C)) / (2 |^ p) is V11() real ext-real Element of REAL

((N-bound C) - (S-bound C)) * ((2 |^ p) ") is V11() real ext-real set

(width (Gauge (C,p))) - 2 is V11() real ext-real Element of REAL

(width (Gauge (C,p))) + (- 2) is V11() real ext-real set

(((N-bound C) - (S-bound C)) / (2 |^ p)) * ((width (Gauge (C,p))) - 2) is V11() real ext-real Element of REAL

(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ p)) * ((width (Gauge (C,p))) - 2)) is V11() real ext-real Element of REAL

|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ p)) * (p9 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ p)) * ((width (Gauge (C,p))) - 2)))]| is non empty non trivial V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ p)) * (p9 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ p)) * ((width (Gauge (C,p))) - 2)))]| `2 is V11() real ext-real Element of REAL

C is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

p is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

(p + 1) / p is V11() real ext-real non negative Element of REAL

p " is V11() real ext-real non negative set

(p + 1) * (p ") is V11() real ext-real non negative set

C + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

(C + 1) / C is V11() real ext-real non negative Element of REAL

C " is V11() real ext-real non negative set

(C + 1) * (C ") is V11() real ext-real non negative set

1 / p is V11() real ext-real non negative Element of REAL

1 * (p ") is V11() real ext-real non negative set

1 / C is V11() real ext-real non negative Element of REAL

1 * (C ") is V11() real ext-real non negative set

C / C is V11() real ext-real non negative Element of COMPLEX

C * (C ") is V11() real ext-real non negative set

(C / C) + (1 / C) is V11() real ext-real non negative Element of REAL

1 + (1 / C) is non empty V11() real ext-real positive non negative Element of REAL

p / p is V11() real ext-real non negative Element of COMPLEX

p * (p ") is V11() real ext-real non negative set

(p / p) + (1 / p) is V11() real ext-real non negative Element of REAL

1 + (1 / p) is non empty V11() real ext-real positive non negative Element of REAL

C is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

p is non empty functional closed bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))

Gauge (p,C) is V15() non empty-yielding V18( NAT ) V19(K307( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K307( the carrier of (TOP-REAL 2))

width (Gauge (p,C)) is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

Center (Gauge (p,C)) is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

(Gauge (p,C)) * ((Center (Gauge (p,C))),(width (Gauge (p,C)))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

p9 is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

s is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

(Gauge (p,C)) * ((Center (Gauge (p,C))),s) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

LSeg (((Gauge (p,C)) * ((Center (Gauge (p,C))),(width (Gauge (p,C))))),((Gauge (p,C)) * ((Center (Gauge (p,C))),s))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

Gauge (p,p9) is V15() non empty-yielding V18( NAT ) V19(K307( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K307( the carrier of (TOP-REAL 2))

Center (Gauge (p,p9)) is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

width (Gauge (p,p9)) is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

(Gauge (p,p9)) * ((Center (Gauge (p,p9))),(width (Gauge (p,p9)))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

LSeg (((Gauge (p,p9)) * ((Center (Gauge (p,p9))),(width (Gauge (p,p9))))),((Gauge (p,C)) * ((Center (Gauge (p,C))),s))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

N-bound p is V11() real ext-real Element of REAL

(TOP-REAL 2) | p is strict T_2 compact SubSpace of TOP-REAL 2

proj2 | p is V15() V18( the carrier of ((TOP-REAL 2) | p)) V19( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | p), REAL ) V212((TOP-REAL 2) | p) Element of K6(K7( the carrier of ((TOP-REAL 2) | p),REAL))

the carrier of ((TOP-REAL 2) | p) is set

K7( the carrier of ((TOP-REAL 2) | p),REAL) is set

K6(K7( the carrier of ((TOP-REAL 2) | p),REAL)) is non empty set

upper_bound (proj2 | p) is V11() real ext-real Element of REAL

(proj2 | p) .: the carrier of ((TOP-REAL 2) | p) is Element of K6(REAL)

upper_bound ((proj2 | p) .: the carrier of ((TOP-REAL 2) | p)) is V11() real ext-real Element of REAL

S-bound p is V11() real ext-real Element of REAL

lower_bound (proj2 | p) is V11() real ext-real Element of REAL

lower_bound ((proj2 | p) .: the carrier of ((TOP-REAL 2) | p)) is V11() real ext-real Element of REAL

W-bound p is V11() real ext-real Element of REAL

proj1 | p is V15() V18( the carrier of ((TOP-REAL 2) | p)) V19( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | p), REAL ) V212((TOP-REAL 2) | p) Element of K6(K7( the carrier of ((TOP-REAL 2) | p),REAL))

lower_bound (proj1 | p) is V11() real ext-real Element of REAL

(proj1 | p) .: the carrier of ((TOP-REAL 2) | p) is Element of K6(REAL)

lower_bound ((proj1 | p) .: the carrier of ((TOP-REAL 2) | p)) is V11() real ext-real Element of REAL

E-bound p is V11() real ext-real Element of REAL

upper_bound (proj1 | p) is V11() real ext-real Element of REAL

upper_bound ((proj1 | p) .: the carrier of ((TOP-REAL 2) | p)) is V11() real ext-real Element of REAL

len (Gauge (p,p9)) is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

2 |^ p9 is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

(2 |^ p9) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

len (Gauge (p,C)) is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

2 |^ C is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

(2 |^ C) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

m9 is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

(N-bound p) - (S-bound p) is V11() real ext-real Element of REAL

- (S-bound p) is V11() real ext-real set

(N-bound p) + (- (S-bound p)) is V11() real ext-real set

((Gauge (p,p9)) * ((Center (Gauge (p,p9))),(width (Gauge (p,p9))))) `1 is V11() real ext-real Element of REAL

(Gauge (p,C)) * ((Center (Gauge (p,C))),m9) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

((Gauge (p,C)) * ((Center (Gauge (p,C))),m9)) `1 is V11() real ext-real Element of REAL

((Gauge (p,C)) * ((Center (Gauge (p,C))),s)) `1 is V11() real ext-real Element of REAL

[(Center (Gauge (p,C))),m9] is set

{(Center (Gauge (p,C))),m9} is non empty set

{(Center (Gauge (p,C)))} is non empty trivial V35(1) set

{{(Center (Gauge (p,C))),m9},{(Center (Gauge (p,C)))}} is non empty set

Indices (Gauge (p,C)) is set

((Gauge (p,C)) * ((Center (Gauge (p,C))),m9)) `2 is V11() real ext-real Element of REAL

(E-bound p) - (W-bound p) is V11() real ext-real Element of REAL

- (W-bound p) is V11() real ext-real set

(E-bound p) + (- (W-bound p)) is V11() real ext-real set

((E-bound p) - (W-bound p)) / (2 |^ C) is V11() real ext-real Element of REAL

(2 |^ C) " is V11() real ext-real non negative set

((E-bound p) - (W-bound p)) * ((2 |^ C) ") is V11() real ext-real set

(Center (Gauge (p,C))) - 2 is V11() real ext-real Element of REAL

(Center (Gauge (p,C))) + (- 2) is V11() real ext-real set

(((E-bound p) - (W-bound p)) / (2 |^ C)) * ((Center (Gauge (p,C))) - 2) is V11() real ext-real Element of REAL

(W-bound p) + ((((E-bound p) - (W-bound p)) / (2 |^ C)) * ((Center (Gauge (p,C))) - 2)) is V11() real ext-real Element of REAL

((N-bound p) - (S-bound p)) / (2 |^ C) is V11() real ext-real Element of REAL

((N-bound p) - (S-bound p)) * ((2 |^ C) ") is V11() real ext-real set

m9 - 2 is V11() real ext-real Element of REAL

m9 + (- 2) is V11() real ext-real set

(((N-bound p) - (S-bound p)) / (2 |^ C)) * (m9 - 2) is V11() real ext-real Element of REAL

(S-bound p) + ((((N-bound p) - (S-bound p)) / (2 |^ C)) * (m9 - 2)) is V11() real ext-real Element of REAL

|[((W-bound p) + ((((E-bound p) - (W-bound p)) / (2 |^ C)) * ((Center (Gauge (p,C))) - 2))),((S-bound p) + ((((N-bound p) - (S-bound p)) / (2 |^ C)) * (m9 - 2)))]| is non empty non trivial V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

|[((W-bound p) + ((((E-bound p) - (W-bound p)) / (2 |^ C)) * ((Center (Gauge (p,C))) - 2))),((S-bound p) + ((((N-bound p) - (S-bound p)) / (2 |^ C)) * (m9 - 2)))]| `2 is V11() real ext-real Element of REAL

[(Center (Gauge (p,p9))),(width (Gauge (p,p9)))] is set

{(Center (Gauge (p,p9))),(width (Gauge (p,p9)))} is non empty set

{(Center (Gauge (p,p9)))} is non empty trivial V35(1) set

{{(Center (Gauge (p,p9))),(width (Gauge (p,p9)))},{(Center (Gauge (p,p9)))}} is non empty set

Indices (Gauge (p,p9)) is set

((Gauge (p,p9)) * ((Center (Gauge (p,p9))),(width (Gauge (p,p9))))) `2 is V11() real ext-real Element of REAL

((N-bound p) - (S-bound p)) / (2 |^ p9) is V11() real ext-real Element of REAL

(2 |^ p9) " is V11() real ext-real non negative set

((N-bound p) - (S-bound p)) * ((2 |^ p9) ") is V11() real ext-real set

(width (Gauge (p,p9))) - 2 is V11() real ext-real Element of REAL

(width (Gauge (p,p9))) + (- 2) is V11() real ext-real set

(((N-bound p) - (S-bound p)) / (2 |^ p9)) * ((width (Gauge (p,p9))) - 2) is V11() real ext-real Element of REAL

(S-bound p) + ((((N-bound p) - (S-bound p)) / (2 |^ p9)) * ((width (Gauge (p,p9))) - 2)) is V11() real ext-real Element of REAL

(2 |^ C) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

((2 |^ C) + 1) / (2 |^ C) is V11() real ext-real non negative Element of REAL

((2 |^ C) + 1) * ((2 |^ C) ") is V11() real ext-real non negative set

(2 |^ p9) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

((2 |^ p9) + 1) / (2 |^ p9) is V11() real ext-real non negative Element of REAL

((2 |^ p9) + 1) * ((2 |^ p9) ") is V11() real ext-real non negative set

((2 |^ C) + 3) - 2 is V11() real ext-real Element of REAL

((2 |^ C) + 3) + (- 2) is V11() real ext-real set

(m9 - 2) / (2 |^ C) is V11() real ext-real Element of REAL

(m9 - 2) * ((2 |^ C) ") is V11() real ext-real set

((width (Gauge (p,p9))) - 2) / (2 |^ p9) is V11() real ext-real Element of REAL

((width (Gauge (p,p9))) - 2) * ((2 |^ p9) ") is V11() real ext-real set

((N-bound p) - (S-bound p)) * ((m9 - 2) / (2 |^ C)) is V11() real ext-real Element of REAL

((N-bound p) - (S-bound p)) * (((width (Gauge (p,p9))) - 2) / (2 |^ p9)) is V11() real ext-real Element of REAL

((Gauge (p,C)) * ((Center (Gauge (p,C))),s)) `2 is V11() real ext-real Element of REAL

C is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

p is non empty functional closed connected bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))

Gauge (p,C) is V15() non empty-yielding V18( NAT ) V19(K307( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K307( the carrier of (TOP-REAL 2))

len (Gauge (p,C)) is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

width (Gauge (p,C)) is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

Cage (p,C) is non empty non trivial V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like non constant V28() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the carrier of (TOP-REAL 2)

L~ (Cage (p,C)) is non empty functional closed connected bounded being_simple_closed_curve compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))

Upper_Seq (p,C) is non empty non trivial V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like one-to-one V28() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2)

L~ (Upper_Seq (p,C)) is non empty functional closed bounded compact Element of K6( the carrier of (TOP-REAL 2))

p9 is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

s is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

(Gauge (p,C)) * (p9,s) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

(Gauge (p,C)) * (p9,(width (Gauge (p,C)))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

LSeg (((Gauge (p,C)) * (p9,(width (Gauge (p,C))))),((Gauge (p,C)) * (p9,s))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

SW-corner (L~ (Cage (p,C))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

W-bound (L~ (Cage (p,C))) is V11() real ext-real Element of REAL

(TOP-REAL 2) | (L~ (Cage (p,C))) is strict T_2 compact SubSpace of TOP-REAL 2

proj1 | (L~ (Cage (p,C))) is V15() V18( the carrier of ((TOP-REAL 2) | (L~ (Cage (p,C))))) V19( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (p,C)))), REAL ) V212((TOP-REAL 2) | (L~ (Cage (p,C)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (p,C)))),REAL))

the carrier of ((TOP-REAL 2) | (L~ (Cage (p,C)))) is set

K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (p,C)))),REAL) is set

K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (p,C)))),REAL)) is non empty set

lower_bound (proj1 | (L~ (Cage (p,C)))) is V11() real ext-real Element of REAL

(proj1 | (L~ (Cage (p,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (p,C)))) is Element of K6(REAL)

lower_bound ((proj1 | (L~ (Cage (p,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (p,C))))) is V11() real ext-real Element of REAL

S-bound (L~ (Cage (p,C))) is V11() real ext-real Element of REAL

proj2 | (L~ (Cage (p,C))) is V15() V18( the carrier of ((TOP-REAL 2) | (L~ (Cage (p,C))))) V19( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (L~ (Cage (p,C)))), REAL ) V212((TOP-REAL 2) | (L~ (Cage (p,C)))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (L~ (Cage (p,C)))),REAL))

lower_bound (proj2 | (L~ (Cage (p,C)))) is V11() real ext-real Element of REAL

(proj2 | (L~ (Cage (p,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (p,C)))) is Element of K6(REAL)

lower_bound ((proj2 | (L~ (Cage (p,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (p,C))))) is V11() real ext-real Element of REAL

|[(W-bound (L~ (Cage (p,C)))),(S-bound (L~ (Cage (p,C))))]| is non empty non trivial V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

Lower_Seq (p,C) is non empty non trivial V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like one-to-one V28() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2)

L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))) is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> is non empty trivial V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like constant V28() V35(1) FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) is non empty V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

<*(SW-corner (L~ (Cage (p,C))))*> is non empty trivial V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like constant V28() V35(1) FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

(<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*> is non empty V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

len (Upper_Seq (p,C)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

mid ((Upper_Seq (p,C)),2,(len (Upper_Seq (p,C)))) is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

L~ (Lower_Seq (p,C)) is non empty functional closed bounded compact Element of K6( the carrier of (TOP-REAL 2))

(L~ (Lower_Seq (p,C))) \/ (L~ (Upper_Seq (p,C))) is non empty functional Element of K6( the carrier of (TOP-REAL 2))

len (Lower_Seq (p,C)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

((Gauge (p,C)) * (p9,(width (Gauge (p,C))))) `2 is V11() real ext-real Element of REAL

N-bound (L~ (Cage (p,C))) is V11() real ext-real Element of REAL

upper_bound (proj2 | (L~ (Cage (p,C)))) is V11() real ext-real Element of REAL

upper_bound ((proj2 | (L~ (Cage (p,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (p,C))))) is V11() real ext-real Element of REAL

E-max (L~ (Cage (p,C))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

E-bound (L~ (Cage (p,C))) is V11() real ext-real Element of REAL

upper_bound (proj1 | (L~ (Cage (p,C)))) is V11() real ext-real Element of REAL

upper_bound ((proj1 | (L~ (Cage (p,C)))) .: the carrier of ((TOP-REAL 2) | (L~ (Cage (p,C))))) is V11() real ext-real Element of REAL

E-most (L~ (Cage (p,C))) is non empty functional closed bounded compact Element of K6( the carrier of (TOP-REAL 2))

SE-corner (L~ (Cage (p,C))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

|[(E-bound (L~ (Cage (p,C)))),(S-bound (L~ (Cage (p,C))))]| is non empty non trivial V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

NE-corner (L~ (Cage (p,C))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

|[(E-bound (L~ (Cage (p,C)))),(N-bound (L~ (Cage (p,C))))]| is non empty non trivial V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

LSeg ((SE-corner (L~ (Cage (p,C)))),(NE-corner (L~ (Cage (p,C))))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

(LSeg ((SE-corner (L~ (Cage (p,C)))),(NE-corner (L~ (Cage (p,C)))))) /\ (L~ (Cage (p,C))) is functional closed bounded compact Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (E-most (L~ (Cage (p,C)))) is strict T_2 compact SubSpace of TOP-REAL 2

proj2 | (E-most (L~ (Cage (p,C)))) is V15() V18( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (p,C)))))) V19( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (p,C))))), REAL ) V212((TOP-REAL 2) | (E-most (L~ (Cage (p,C))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (p,C))))),REAL))

the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (p,C))))) is set

K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (p,C))))),REAL) is set

K6(K7( the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (p,C))))),REAL)) is non empty set

upper_bound (proj2 | (E-most (L~ (Cage (p,C))))) is V11() real ext-real Element of REAL

(proj2 | (E-most (L~ (Cage (p,C))))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (p,C))))) is Element of K6(REAL)

upper_bound ((proj2 | (E-most (L~ (Cage (p,C))))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ (Cage (p,C)))))) is V11() real ext-real Element of REAL

|[(E-bound (L~ (Cage (p,C)))),(upper_bound (proj2 | (E-most (L~ (Cage (p,C))))))]| is non empty non trivial V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

(Gauge (p,C)) * ((len (Gauge (p,C))),(width (Gauge (p,C)))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

((Gauge (p,C)) * ((len (Gauge (p,C))),(width (Gauge (p,C))))) `1 is V11() real ext-real Element of REAL

(E-max (L~ (Cage (p,C)))) `1 is V11() real ext-real Element of REAL

((Gauge (p,C)) * ((len (Gauge (p,C))),(width (Gauge (p,C))))) `2 is V11() real ext-real Element of REAL

(E-max (L~ (Cage (p,C)))) `2 is V11() real ext-real Element of REAL

((Gauge (p,C)) * (p9,s)) `1 is V11() real ext-real Element of REAL

((Gauge (p,C)) * (p9,s)) `2 is V11() real ext-real Element of REAL

(Gauge (p,C)) * ((len (Gauge (p,C))),s) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

LSeg (((Gauge (p,C)) * ((len (Gauge (p,C))),(width (Gauge (p,C))))),((Gauge (p,C)) * ((len (Gauge (p,C))),s))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

rng (Upper_Seq (p,C)) is functional Element of K6( the carrier of (TOP-REAL 2))

(Upper_Seq (p,C)) /. (len (Upper_Seq (p,C))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

(Lower_Seq (p,C)) . (len (Lower_Seq (p,C))) is V15() Function-like set

W-min (L~ (Cage (p,C))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

W-most (L~ (Cage (p,C))) is non empty functional closed bounded compact Element of K6( the carrier of (TOP-REAL 2))

NW-corner (L~ (Cage (p,C))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

|[(W-bound (L~ (Cage (p,C)))),(N-bound (L~ (Cage (p,C))))]| is non empty non trivial V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

LSeg ((SW-corner (L~ (Cage (p,C)))),(NW-corner (L~ (Cage (p,C))))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

(LSeg ((SW-corner (L~ (Cage (p,C)))),(NW-corner (L~ (Cage (p,C)))))) /\ (L~ (Cage (p,C))) is functional closed bounded compact Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (W-most (L~ (Cage (p,C)))) is strict T_2 compact SubSpace of TOP-REAL 2

proj2 | (W-most (L~ (Cage (p,C)))) is V15() V18( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (p,C)))))) V19( REAL ) Function-like V40( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (p,C))))), REAL ) V212((TOP-REAL 2) | (W-most (L~ (Cage (p,C))))) Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (p,C))))),REAL))

the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (p,C))))) is set

K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (p,C))))),REAL) is set

K6(K7( the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (p,C))))),REAL)) is non empty set

lower_bound (proj2 | (W-most (L~ (Cage (p,C))))) is V11() real ext-real Element of REAL

(proj2 | (W-most (L~ (Cage (p,C))))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (p,C))))) is Element of K6(REAL)

lower_bound ((proj2 | (W-most (L~ (Cage (p,C))))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ (Cage (p,C)))))) is V11() real ext-real Element of REAL

|[(W-bound (L~ (Cage (p,C)))),(lower_bound (proj2 | (W-most (L~ (Cage (p,C))))))]| is non empty non trivial V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

len (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

dom (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) is Element of K6(NAT)

dom (Lower_Seq (p,C)) is non trivial Element of K6(NAT)

(L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) /. (len (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

(L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) . (len (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) is V15() Function-like set

(Lower_Seq (p,C)) /. (len (Lower_Seq (p,C))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

len (<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

(<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) /. (len (<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

(L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) /. 1 is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

(L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) . 1 is V15() Function-like set

(L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) ^ <*(SW-corner (L~ (Cage (p,C))))*> is non empty V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

((L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) ^ <*(SW-corner (L~ (Cage (p,C))))*>) /. 1 is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

1 + (len (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

len ((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

(len (<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

(1 + (len (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

Rev ((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>) is non empty V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

len (Rev ((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

{((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))} is non empty trivial functional V35(1) set

rng <*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> is trivial functional Element of K6( the carrier of (TOP-REAL 2))

len (Cage (p,C)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

rng (Cage (p,C)) is non trivial functional Element of K6( the carrier of (TOP-REAL 2))

(SW-corner (L~ (Cage (p,C)))) `1 is V11() real ext-real Element of REAL

(SW-corner (L~ (Cage (p,C)))) `2 is V11() real ext-real Element of REAL

{ b

(W-min (L~ (Cage (p,C)))) `2 is V11() real ext-real Element of REAL

(W-min (L~ (Cage (p,C)))) `1 is V11() real ext-real Element of REAL

Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C))) is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

(Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

(Lower_Seq (p,C)) . ((Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1) is V15() Function-like set

<*((Gauge (p,C)) * (p9,s))*> is non empty trivial V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like constant V28() V35(1) FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

mid ((Lower_Seq (p,C)),((Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1),(len (Lower_Seq (p,C)))) is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

<*((Gauge (p,C)) * (p9,s))*> ^ (mid ((Lower_Seq (p,C)),((Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1),(len (Lower_Seq (p,C))))) is non empty V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

rng (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) is functional Element of K6( the carrier of (TOP-REAL 2))

rng <*((Gauge (p,C)) * (p9,s))*> is trivial functional Element of K6( the carrier of (TOP-REAL 2))

rng (mid ((Lower_Seq (p,C)),((Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1),(len (Lower_Seq (p,C))))) is functional Element of K6( the carrier of (TOP-REAL 2))

(rng <*((Gauge (p,C)) * (p9,s))*>) \/ (rng (mid ((Lower_Seq (p,C)),((Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1),(len (Lower_Seq (p,C)))))) is functional Element of K6( the carrier of (TOP-REAL 2))

{((Gauge (p,C)) * (p9,s))} is non empty trivial functional V35(1) set

{((Gauge (p,C)) * (p9,s))} \/ (rng (mid ((Lower_Seq (p,C)),((Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1),(len (Lower_Seq (p,C)))))) is non empty set

N is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

N + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

(Cage (p,C)) /. N is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

(Cage (p,C)) /. (N + 1) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

LSeg (((Cage (p,C)) /. N),((Cage (p,C)) /. (N + 1))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

((Cage (p,C)) /. N) `1 is V11() real ext-real Element of REAL

((Cage (p,C)) /. (N + 1)) `1 is V11() real ext-real Element of REAL

(SW-corner (L~ (Cage (p,C)))) `1 is V11() real ext-real Element of REAL

(SW-corner (L~ (Cage (p,C)))) `2 is V11() real ext-real Element of REAL

((Cage (p,C)) /. N) `2 is V11() real ext-real Element of REAL

((Cage (p,C)) /. (N + 1)) `2 is V11() real ext-real Element of REAL

dom (Cage (p,C)) is non trivial Element of K6(NAT)

((Cage (p,C)) /. N) `2 is V11() real ext-real Element of REAL

((Cage (p,C)) /. (N + 1)) `2 is V11() real ext-real Element of REAL

(SW-corner (L~ (Cage (p,C)))) `2 is V11() real ext-real Element of REAL

(SW-corner (L~ (Cage (p,C)))) `1 is V11() real ext-real Element of REAL

((Cage (p,C)) /. N) `1 is V11() real ext-real Element of REAL

((Cage (p,C)) /. (N + 1)) `1 is V11() real ext-real Element of REAL

dom (Cage (p,C)) is non trivial Element of K6(NAT)

((Cage (p,C)) /. N) `1 is V11() real ext-real Element of REAL

((Cage (p,C)) /. (N + 1)) `1 is V11() real ext-real Element of REAL

((Cage (p,C)) /. N) `2 is V11() real ext-real Element of REAL

((Cage (p,C)) /. (N + 1)) `2 is V11() real ext-real Element of REAL

rng (Lower_Seq (p,C)) is functional Element of K6( the carrier of (TOP-REAL 2))

Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C))) is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

(Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

(Lower_Seq (p,C)) . ((Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1) is V15() Function-like set

mid ((Lower_Seq (p,C)),((Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1),(len (Lower_Seq (p,C)))) is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

rng (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) is functional Element of K6( the carrier of (TOP-REAL 2))

rng (Lower_Seq (p,C)) is functional Element of K6( the carrier of (TOP-REAL 2))

Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C))) is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

(Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

(Lower_Seq (p,C)) . ((Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1) is V15() Function-like set

rng (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) is functional Element of K6( the carrier of (TOP-REAL 2))

rng (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) is functional Element of K6( the carrier of (TOP-REAL 2))

(rng <*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*>) \/ (rng (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) is functional Element of K6( the carrier of (TOP-REAL 2))

rng (<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) is functional Element of K6( the carrier of (TOP-REAL 2))

{(SW-corner (L~ (Cage (p,C))))} is non empty trivial functional V35(1) set

rng <*(SW-corner (L~ (Cage (p,C))))*> is trivial functional Element of K6( the carrier of (TOP-REAL 2))

rng (Lower_Seq (p,C)) is functional Element of K6( the carrier of (TOP-REAL 2))

{((Gauge (p,C)) * (p9,s))} is non empty trivial functional V35(1) set

<*((Gauge (p,C)) * (p9,s))*> is non empty trivial V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like constant V28() V35(1) FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

rng <*((Gauge (p,C)) * (p9,s))*> is trivial functional Element of K6( the carrier of (TOP-REAL 2))

Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C))) is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

(Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

mid ((Lower_Seq (p,C)),((Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1),(len (Lower_Seq (p,C)))) is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

(Lower_Seq (p,C)) . ((Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1) is V15() Function-like set

rng (mid ((Lower_Seq (p,C)),((Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1),(len (Lower_Seq (p,C))))) is functional Element of K6( the carrier of (TOP-REAL 2))

(rng <*((Gauge (p,C)) * (p9,s))*>) \/ (rng (mid ((Lower_Seq (p,C)),((Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1),(len (Lower_Seq (p,C)))))) is functional Element of K6( the carrier of (TOP-REAL 2))

<*((Gauge (p,C)) * (p9,s))*> ^ (mid ((Lower_Seq (p,C)),((Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1),(len (Lower_Seq (p,C))))) is non empty V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

rng (<*((Gauge (p,C)) * (p9,s))*> ^ (mid ((Lower_Seq (p,C)),((Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1),(len (Lower_Seq (p,C)))))) is functional Element of K6( the carrier of (TOP-REAL 2))

(Lower_Seq (p,C)) . ((Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1) is V15() Function-like set

(Lower_Seq (p,C)) . ((Index (((Gauge (p,C)) * (p9,s)),(Lower_Seq (p,C)))) + 1) is V15() Function-like set

len <*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> /. (len <*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*>) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

(<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> /. (len <*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*>)) `1 is V11() real ext-real Element of REAL

<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> /. 1 is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

(<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> /. 1) `1 is V11() real ext-real Element of REAL

((Gauge (p,C)) * (p9,(width (Gauge (p,C))))) `1 is V11() real ext-real Element of REAL

(Gauge (p,C)) * (p9,1) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

((Gauge (p,C)) * (p9,1)) `1 is V11() real ext-real Element of REAL

((L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) /. 1) `1 is V11() real ext-real Element of REAL

((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) /. (len (<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))))) `1 is V11() real ext-real Element of REAL

(SW-corner (L~ (Cage (p,C)))) `1 is V11() real ext-real Element of REAL

<*(SW-corner (L~ (Cage (p,C))))*> /. 1 is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

(<*(SW-corner (L~ (Cage (p,C))))*> /. 1) `1 is V11() real ext-real Element of REAL

2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real positive non negative Element of NAT

len (mid ((Upper_Seq (p,C)),2,(len (Upper_Seq (p,C))))) is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

dom (Upper_Seq (p,C)) is non trivial Element of K6(NAT)

(Upper_Seq (p,C)) /. (len (Upper_Seq (p,C))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

((Upper_Seq (p,C)) /. (len (Upper_Seq (p,C)))) `1 is V11() real ext-real Element of REAL

(mid ((Upper_Seq (p,C)),2,(len (Upper_Seq (p,C))))) /. (len (mid ((Upper_Seq (p,C)),2,(len (Upper_Seq (p,C)))))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

((mid ((Upper_Seq (p,C)),2,(len (Upper_Seq (p,C))))) /. (len (mid ((Upper_Seq (p,C)),2,(len (Upper_Seq (p,C))))))) `1 is V11() real ext-real Element of REAL

(Upper_Seq (p,C)) /. (1 + 1) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

((Upper_Seq (p,C)) /. (1 + 1)) `1 is V11() real ext-real Element of REAL

(mid ((Upper_Seq (p,C)),2,(len (Upper_Seq (p,C))))) /. 1 is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

((mid ((Upper_Seq (p,C)),2,(len (Upper_Seq (p,C))))) /. 1) `1 is V11() real ext-real Element of REAL

m is epsilon-transitive epsilon-connected ordinal natural V11() real V28() V33() ext-real non negative Element of NAT

dom <*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> is non empty trivial V35(1) Element of K6(NAT)

<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> . m is V15() Function-like set

<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> /. m is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

(Gauge (p,C)) * (1,(width (Gauge (p,C)))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

((Gauge (p,C)) * (1,(width (Gauge (p,C))))) `1 is V11() real ext-real Element of REAL

(<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> /. m) `1 is V11() real ext-real Element of REAL

(Gauge (p,C)) * ((len (Gauge (p,C))),(width (Gauge (p,C)))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

((Gauge (p,C)) * ((len (Gauge (p,C))),(width (Gauge (p,C))))) `1 is V11() real ext-real Element of REAL

(<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> /. m) `2 is V11() real ext-real Element of REAL

<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ ((L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) ^ <*(SW-corner (L~ (Cage (p,C))))*>) is non empty V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>) /. 1 is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

(((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>) /. 1) `2 is V11() real ext-real Element of REAL

(Rev ((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>)) /. (len ((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>)) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

((Rev ((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>)) /. (len ((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>))) `2 is V11() real ext-real Element of REAL

(Rev ((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>)) /. (len (Rev ((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>))) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

((Rev ((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>)) /. (len (Rev ((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>)))) `2 is V11() real ext-real Element of REAL

((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>) /. (len ((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>)) is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

(((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>) /. (len ((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>))) `2 is V11() real ext-real Element of REAL

(Rev ((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>)) /. 1 is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

((Rev ((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>)) /. 1) `2 is V11() real ext-real Element of REAL

L~ (mid ((Upper_Seq (p,C)),2,(len (Upper_Seq (p,C))))) is functional closed bounded compact Element of K6( the carrier of (TOP-REAL 2))

L~ (Rev ((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>)) is functional closed bounded compact Element of K6( the carrier of (TOP-REAL 2))

L~ ((<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) ^ <*(SW-corner (L~ (Cage (p,C))))*>) is functional closed bounded compact Element of K6( the carrier of (TOP-REAL 2))

m is set

L~ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) is functional closed bounded compact Element of K6( the carrier of (TOP-REAL 2))

L~ (<*((Gauge (p,C)) * (p9,(width (Gauge (p,C)))))*> ^ ((L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) ^ <*(SW-corner (L~ (Cage (p,C))))*>)) is functional closed bounded compact Element of K6( the carrier of (TOP-REAL 2))

LSeg (((Gauge (p,C)) * (p9,(width (Gauge (p,C))))),(((L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) ^ <*(SW-corner (L~ (Cage (p,C))))*>) /. 1)) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

L~ ((L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) ^ <*(SW-corner (L~ (Cage (p,C))))*>) is functional closed bounded compact Element of K6( the carrier of (TOP-REAL 2))

(LSeg (((Gauge (p,C)) * (p9,(width (Gauge (p,C))))),(((L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) ^ <*(SW-corner (L~ (Cage (p,C))))*>) /. 1))) \/ (L~ ((L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) ^ <*(SW-corner (L~ (Cage (p,C))))*>)) is non empty functional Element of K6( the carrier of (TOP-REAL 2))

LSeg (((L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) /. (len (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))))),(SW-corner (L~ (Cage (p,C))))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

(L~ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) \/ (LSeg (((L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) /. (len (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))))),(SW-corner (L~ (Cage (p,C)))))) is non empty functional Element of K6( the carrier of (TOP-REAL 2))

(LSeg (((Gauge (p,C)) * (p9,(width (Gauge (p,C))))),(((L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) ^ <*(SW-corner (L~ (Cage (p,C))))*>) /. 1))) \/ ((L~ (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s))))) \/ (LSeg (((L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))) /. (len (L_Cut ((Lower_Seq (p,C)),((Gauge (p,C)) * (p9,s)))))),(SW-corner (L~ (Cage (p,C))))))) is non empty functional Element of K6( the carrier of (TOP-REAL 2))

(Upper_Seq (p,C)) /. 1 is V15() V18( NAT ) Function-like V28() V35(2) FinSequence-like FinSubsequence-like V168() Element of the carrier of (TOP-REAL 2)

<*((Gauge (p,C)) * (p9,(width (Gauge (p,C))))),((Gauge (p,C)) * (p9,s))*> is non empty non trivial V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V28() V35(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

L~ <*((Gauge (p,C)) * (p9,(width (Gauge (p,C))))),((Gauge (p,C)) * (p9,s))*> is non empty functional closed bounded compact Element of K6( the carrier of (TOP-REAL 2))

(L~ (Lower_Seq (p,C))) /\ (L~ (Upper_Seq (p,C))) is functional closed bounded compact Element of K6( the carrier of (TOP-REAL 2))

{(W-min (L~ (Cage (p,C)))),(E-max (L~ (Cage (p,C))))} is non empty functional set

(Lower_Seq (p,C)) . 1 is V15() Function-like set

(Lower_Seq (p,C)) /. 1 is V15() V18(