REAL is non empty V26() V144() V145() V146() V150() set
NAT is non empty V4() V5() V6() V144() V145() V146() V147() V148() V149() V150() Element of K6(REAL)
K6(REAL) is set
NAT is non empty V4() V5() V6() V144() V145() V146() V147() V148() V149() V150() set
K6(NAT) is set
K6(NAT) is set
COMPLEX is non empty V26() V144() V150() set
1 is non empty V4() V5() V6() V10() V11() V12() V37() ext-real positive V97() V144() V145() V146() V147() V148() V149() Element of NAT
K7(1,1) is set
K6(K7(1,1)) is set
K7(K7(1,1),1) is set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty V4() V5() V6() V10() V11() V12() V37() ext-real positive V97() V144() V145() V146() V147() V148() V149() Element of NAT
K7(2,2) is set
K7(K7(2,2),REAL) is set
K6(K7(K7(2,2),REAL)) is set
RAT is non empty V26() V144() V145() V146() V147() V150() set
INT is non empty V26() V144() V145() V146() V147() V148() V150() set
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V110() V156() V157() V158() V159() V160() V161() V162() 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 set
K6( the carrier of (TOP-REAL 2)) is set
K338( the carrier of (TOP-REAL 2)) is non empty V21() FinSequence-membered M11( the carrier of (TOP-REAL 2))
{} is empty V4() V5() V6() V8() V9() V10() V12() V21() FinSequence-membered V37() V144() V145() V146() V147() V148() V149() V150() set
3 is non empty V4() V5() V6() V10() V11() V12() V37() ext-real positive V97() V144() V145() V146() V147() V148() V149() Element of NAT
0 is empty V4() V5() V6() V8() V9() V10() V11() V12() V21() FinSequence-membered V37() ext-real V97() V144() V145() V146() V147() V148() V149() V150() Element of NAT
1 / 2 is V11() V12() ext-real Element of REAL
4 is non empty V4() V5() V6() V10() V11() V12() V37() ext-real positive V97() V144() V145() V146() V147() V148() V149() Element of NAT
len {} is V31() set
C is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ C is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ C) is open Element of K6( the carrier of (TOP-REAL 2))
RightComp C is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
LeftComp C is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
(L~ C) ` is open dense Element of K6( the carrier of (TOP-REAL 2))
C is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ C is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
UBD (L~ C) is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
RightComp C is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
LeftComp C is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
(L~ C) ` is open dense Element of K6( the carrier of (TOP-REAL 2))
C is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
n is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
left_cell (n,m,C) is Element of K6( the carrier of (TOP-REAL 2))
Indices C is set
n /. m is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
n /. (m + 1) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
G is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
f is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
[G,f] is set
{G,f} is non empty V144() V145() V146() V147() V148() V149() set
{G} is non empty V144() V145() V146() V147() V148() V149() set
{{G,f},{G}} is non empty set
C * (G,f) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
p is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
i1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
[p,i1] is set
{p,i1} is non empty V144() V145() V146() V147() V148() V149() set
{p} is non empty V144() V145() V146() V147() V148() V149() set
{{p,i1},{p}} is non empty set
C * (p,i1) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
f + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
G + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
p + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
i1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
G -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell (C,(G -' 1),f) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,G,f) is Element of K6( the carrier of (TOP-REAL 2))
i1 -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell (C,p,(i1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,G,i1) is Element of K6( the carrier of (TOP-REAL 2))
C is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
len C is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
width C is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
n is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
n `1 is V11() V12() ext-real Element of REAL
n `2 is V11() V12() ext-real Element of REAL
m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
G is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
G + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell (C,m,G) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell (C,m,G)) is open Element of K6( the carrier of (TOP-REAL 2))
C * (m,G) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(C * (m,G)) `1 is V11() V12() ext-real Element of REAL
C * ((m + 1),G) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(C * ((m + 1),G)) `1 is V11() V12() ext-real Element of REAL
(C * (m,G)) `2 is V11() V12() ext-real Element of REAL
C * (m,(G + 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(C * (m,(G + 1))) `2 is V11() V12() ext-real Element of REAL
C * (m,1) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(C * (m,1)) `1 is V11() V12() ext-real Element of REAL
C * ((m + 1),1) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(C * ((m + 1),1)) `1 is V11() V12() ext-real Element of REAL
C * (1,G) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(C * (1,G)) `2 is V11() V12() ext-real Element of REAL
C * (1,(G + 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(C * (1,(G + 1))) `2 is V11() V12() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() V12() ext-real Element of REAL : ( not b1 <= (C * (m,1)) `1 & not (C * ((m + 1),1)) `1 <= b1 & not b2 <= (C * (1,G)) `2 & not (C * (1,(G + 1))) `2 <= b2 ) } is set
p is V11() V12() ext-real Element of REAL
i1 is V11() V12() ext-real Element of REAL
|[p,i1]| is non empty V13() V16( NAT ) V18() V26() V33(2) FinSequence-like FinSubsequence-like V136() Element of the carrier of (TOP-REAL 2)
|[(n `1),(n `2)]| is non empty V13() V16( NAT ) V18() V26() V33(2) FinSequence-like FinSubsequence-like V136() Element of the carrier of (TOP-REAL 2)
C is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ C is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ C) is open Element of K6( the carrier of (TOP-REAL 2))
RightComp C is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
LeftComp C is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
C is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ C is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ C) is open Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Gauge (C,n) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
X-SpanStart (C,n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Y-SpanStart (C,n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
BDD C is open Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(C,n) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
Gauge (C,n) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
X-SpanStart (C,n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Y-SpanStart (C,n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(X-SpanStart (C,n)) -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
len (Gauge (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
width (Gauge (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((X-SpanStart (C,n)) -' 1) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(Y-SpanStart (C,n))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n)))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(Y-SpanStart (C,n))))) is non empty boundary connected convex Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
len (Span (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Gauge (C,n) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
right_cell ((Span (C,n)),m,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
left_cell ((Span (C,n)),m,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
(Span (C,n)) | (len (Span (C,n))) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(Span (C,n)) /. 2 is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
X-SpanStart (C,n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(X-SpanStart (C,n)) -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Y-SpanStart (C,n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Span (C,n)) /. 1 is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
p is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) | p is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len ((Span (C,n)) | p) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
p + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) | (p + 1) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len ((Span (C,n)) | (p + 1)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
i1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
i1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
right_cell (((Span (C,n)) | (p + 1)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
left_cell (((Span (C,n)) | (p + 1)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
i1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
i1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
right_cell (((Span (C,n)) | (p + 1)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
left_cell (((Span (C,n)) | (p + 1)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
0 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
<*((Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n)))),((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))))*> is non empty V13() V16( NAT ) V18() V26() V33(2) FinSequence-like FinSubsequence-like set
((Span (C,n)) | (p + 1)) /. 1 is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
[((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))] is set
{((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))} is non empty V144() V145() V146() V147() V148() V149() set
{((X-SpanStart (C,n)) -' 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))},{((X-SpanStart (C,n)) -' 1)}} is non empty set
Indices (Gauge (C,n)) is set
[(X-SpanStart (C,n)),(Y-SpanStart (C,n))] is set
{(X-SpanStart (C,n)),(Y-SpanStart (C,n))} is non empty V144() V145() V146() V147() V148() V149() set
{(X-SpanStart (C,n))} is non empty V144() V145() V146() V147() V148() V149() set
{{(X-SpanStart (C,n)),(Y-SpanStart (C,n))},{(X-SpanStart (C,n))}} is non empty set
(X-SpanStart (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Y-SpanStart (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
((Span (C,n)) | (p + 1)) /. 2 is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
(Y-SpanStart (C,n)) -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(len ((Span (C,n)) | p)) -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
((len ((Span (C,n)) | p)) -' 1) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
((len ((Span (C,n)) | p)) -' 1) + (1 + 1) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(len ((Span (C,n)) | p)) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
left_cell (((Span (C,n)) | p),((len ((Span (C,n)) | p)) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
left_cell ((Span (C,n)),((len ((Span (C,n)) | p)) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
Indices (Gauge (C,n)) is set
(Span (C,n)) /. ((len ((Span (C,n)) | p)) -' 1) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Span (C,n)) /. (len ((Span (C,n)) | p)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
D is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
[D,j2] is set
{D,j2} is non empty V144() V145() V146() V147() V148() V149() set
{D} is non empty V144() V145() V146() V147() V148() V149() set
{{D,j2},{D}} is non empty set
(Gauge (C,n)) * (D,j2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
i4 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j4 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
[i4,j4] is set
{i4,j4} is non empty V144() V145() V146() V147() V148() V149() set
{i4} is non empty V144() V145() V146() V147() V148() V149() set
{{i4,j4},{i4}} is non empty set
(Gauge (C,n)) * (i4,j4) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
j2 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
D + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
i4 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j4 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
i4 -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(i4 -' 1) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j4 -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(j4 -' 1) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
right_cell (((Span (C,n)) | p),((len ((Span (C,n)) | p)) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
right_cell ((Span (C,n)),((len ((Span (C,n)) | p)) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
front_right_cell ((Span (C,n)),((len ((Span (C,n)) | p)) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
front_left_cell ((Span (C,n)),((len ((Span (C,n)) | p)) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
[(i4 -' 1),j4] is set
{(i4 -' 1),j4} is non empty V144() V145() V146() V147() V148() V149() set
{(i4 -' 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{(i4 -' 1),j4},{(i4 -' 1)}} is non empty set
((len ((Span (C,n)) | p)) -' 1) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) /. (((len ((Span (C,n)) | p)) -' 1) + 2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * ((i4 -' 1),j4) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
D -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),(D -' 1),(j2 + 1)) is Element of K6( the carrier of (TOP-REAL 2))
right_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
(j2 + 1) -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),(D -' 1),j2) is Element of K6( the carrier of (TOP-REAL 2))
left_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
[i4,(j4 + 1)] is set
{i4,(j4 + 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{i4,(j4 + 1)},{i4}} is non empty set
((len ((Span (C,n)) | p)) -' 1) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) /. (((len ((Span (C,n)) | p)) -' 1) + 2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * (i4,(j4 + 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
cell ((Gauge (C,n)),i4,j4) is Element of K6( the carrier of (TOP-REAL 2))
right_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
(D + 1) -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),D,j4) is Element of K6( the carrier of (TOP-REAL 2))
left_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
[i4,(j4 -' 1)] is set
{i4,(j4 -' 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{i4,(j4 -' 1)},{i4}} is non empty set
((len ((Span (C,n)) | p)) -' 1) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) /. (((len ((Span (C,n)) | p)) -' 1) + 2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * (i4,(j4 -' 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
cell ((Gauge (C,n)),(i4 -' 1),(j4 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
right_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),i4,(j4 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
left_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
[(i4 + 1),j4] is set
{(i4 + 1),j4} is non empty V144() V145() V146() V147() V148() V149() set
{(i4 + 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{(i4 + 1),j4},{(i4 + 1)}} is non empty set
((len ((Span (C,n)) | p)) -' 1) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) /. (((len ((Span (C,n)) | p)) -' 1) + 2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * ((i4 + 1),j4) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
cell ((Gauge (C,n)),D,(j4 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
right_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),D,j4) is Element of K6( the carrier of (TOP-REAL 2))
left_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
[(i4 -' 1),j4] is set
{(i4 -' 1),j4} is non empty V144() V145() V146() V147() V148() V149() set
{(i4 -' 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{(i4 -' 1),j4},{(i4 -' 1)}} is non empty set
((len ((Span (C,n)) | p)) -' 1) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) /. (((len ((Span (C,n)) | p)) -' 1) + 2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * ((i4 -' 1),j4) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
[i4,(j4 + 1)] is set
{i4,(j4 + 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{i4,(j4 + 1)},{i4}} is non empty set
(Gauge (C,n)) * (i4,(j4 + 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
[i4,(j4 -' 1)] is set
{i4,(j4 -' 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{i4,(j4 -' 1)},{i4}} is non empty set
(Gauge (C,n)) * (i4,(j4 -' 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
[(i4 + 1),j4] is set
{(i4 + 1),j4} is non empty V144() V145() V146() V147() V148() V149() set
{(i4 + 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{(i4 + 1),j4},{(i4 + 1)}} is non empty set
(Gauge (C,n)) * ((i4 + 1),j4) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
front_right_cell ((Span (C,n)),((len ((Span (C,n)) | p)) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
front_left_cell ((Span (C,n)),((len ((Span (C,n)) | p)) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
[i4,(j4 + 1)] is set
{i4,(j4 + 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{i4,(j4 + 1)},{i4}} is non empty set
((len ((Span (C,n)) | p)) -' 1) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) /. (((len ((Span (C,n)) | p)) -' 1) + 2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * (i4,(j4 + 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
cell ((Gauge (C,n)),D,(j2 + 1)) is Element of K6( the carrier of (TOP-REAL 2))
right_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),(i4 -' 1),j4) is Element of K6( the carrier of (TOP-REAL 2))
left_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
[(i4 + 1),j4] is set
{(i4 + 1),j4} is non empty V144() V145() V146() V147() V148() V149() set
{(i4 + 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{(i4 + 1),j4},{(i4 + 1)}} is non empty set
((len ((Span (C,n)) | p)) -' 1) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) /. (((len ((Span (C,n)) | p)) -' 1) + 2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * ((i4 + 1),j4) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
j2 -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),(D + 1),(j2 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
right_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),(D + 1),j2) is Element of K6( the carrier of (TOP-REAL 2))
left_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
[(i4 -' 1),j4] is set
{(i4 -' 1),j4} is non empty V144() V145() V146() V147() V148() V149() set
{(i4 -' 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{(i4 -' 1),j4},{(i4 -' 1)}} is non empty set
((len ((Span (C,n)) | p)) -' 1) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) /. (((len ((Span (C,n)) | p)) -' 1) + 2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * ((i4 -' 1),j4) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
cell ((Gauge (C,n)),(i4 -' 1),j4) is Element of K6( the carrier of (TOP-REAL 2))
right_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),(i4 -' 1),(j4 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
left_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
[i4,(j4 -' 1)] is set
{i4,(j4 -' 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{i4,(j4 -' 1)},{i4}} is non empty set
((len ((Span (C,n)) | p)) -' 1) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) /. (((len ((Span (C,n)) | p)) -' 1) + 2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * (i4,(j4 -' 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
cell ((Gauge (C,n)),(i4 -' 1),(j4 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
right_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),i4,(j4 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
left_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
[i4,(j4 + 1)] is set
{i4,(j4 + 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{i4,(j4 + 1)},{i4}} is non empty set
((len ((Span (C,n)) | p)) -' 1) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) /. (((len ((Span (C,n)) | p)) -' 1) + 2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * (i4,(j4 + 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
[(i4 + 1),j4] is set
{(i4 + 1),j4} is non empty V144() V145() V146() V147() V148() V149() set
{(i4 + 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{(i4 + 1),j4},{(i4 + 1)}} is non empty set
(Gauge (C,n)) * ((i4 + 1),j4) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
[(i4 -' 1),j4] is set
{(i4 -' 1),j4} is non empty V144() V145() V146() V147() V148() V149() set
{(i4 -' 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{(i4 -' 1),j4},{(i4 -' 1)}} is non empty set
(Gauge (C,n)) * ((i4 -' 1),j4) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
[i4,(j4 -' 1)] is set
{i4,(j4 -' 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{i4,(j4 -' 1)},{i4}} is non empty set
(Gauge (C,n)) * (i4,(j4 -' 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
front_right_cell ((Span (C,n)),((len ((Span (C,n)) | p)) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
[(i4 + 1),j4] is set
{(i4 + 1),j4} is non empty V144() V145() V146() V147() V148() V149() set
{(i4 + 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{(i4 + 1),j4},{(i4 + 1)}} is non empty set
((len ((Span (C,n)) | p)) -' 1) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) /. (((len ((Span (C,n)) | p)) -' 1) + 2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * ((i4 + 1),j4) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(j2 + 1) -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),D,j2) is Element of K6( the carrier of (TOP-REAL 2))
right_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),i4,j4) is Element of K6( the carrier of (TOP-REAL 2))
left_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
[i4,(j4 -' 1)] is set
{i4,(j4 -' 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{i4,(j4 -' 1)},{i4}} is non empty set
((len ((Span (C,n)) | p)) -' 1) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) /. (((len ((Span (C,n)) | p)) -' 1) + 2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * (i4,(j4 -' 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(D + 1) -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j2 -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),D,(j2 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
right_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),i4,(j4 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
left_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
[i4,(j4 + 1)] is set
{i4,(j4 + 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{i4,(j4 + 1)},{i4}} is non empty set
((len ((Span (C,n)) | p)) -' 1) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) /. (((len ((Span (C,n)) | p)) -' 1) + 2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * (i4,(j4 + 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
cell ((Gauge (C,n)),i4,j4) is Element of K6( the carrier of (TOP-REAL 2))
right_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),(i4 -' 1),j4) is Element of K6( the carrier of (TOP-REAL 2))
left_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
[(i4 -' 1),j4] is set
{(i4 -' 1),j4} is non empty V144() V145() V146() V147() V148() V149() set
{(i4 -' 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{(i4 -' 1),j4},{(i4 -' 1)}} is non empty set
((len ((Span (C,n)) | p)) -' 1) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) /. (((len ((Span (C,n)) | p)) -' 1) + 2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * ((i4 -' 1),j4) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
cell ((Gauge (C,n)),(i4 -' 1),j4) is Element of K6( the carrier of (TOP-REAL 2))
right_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),(i4 -' 1),(j4 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
left_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
[(i4 + 1),j4] is set
{(i4 + 1),j4} is non empty V144() V145() V146() V147() V148() V149() set
{(i4 + 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{(i4 + 1),j4},{(i4 + 1)}} is non empty set
((len ((Span (C,n)) | p)) -' 1) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) /. (((len ((Span (C,n)) | p)) -' 1) + 2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * ((i4 + 1),j4) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
[i4,(j4 -' 1)] is set
{i4,(j4 -' 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{i4,(j4 -' 1)},{i4}} is non empty set
(Gauge (C,n)) * (i4,(j4 -' 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
[i4,(j4 + 1)] is set
{i4,(j4 + 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{i4,(j4 + 1)},{i4}} is non empty set
(Gauge (C,n)) * (i4,(j4 + 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
[(i4 -' 1),j4] is set
{(i4 -' 1),j4} is non empty V144() V145() V146() V147() V148() V149() set
{(i4 -' 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{(i4 -' 1),j4},{(i4 -' 1)}} is non empty set
(Gauge (C,n)) * ((i4 -' 1),j4) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
front_right_cell ((Span (C,n)),((len ((Span (C,n)) | p)) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
front_left_cell ((Span (C,n)),((len ((Span (C,n)) | p)) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
Indices (Gauge (C,n)) is set
((Span (C,n)) | p) /. i1 is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((Span (C,n)) | p) /. (i1 + 1) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
D is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
[D,j2] is set
{D,j2} is non empty V144() V145() V146() V147() V148() V149() set
{D} is non empty V144() V145() V146() V147() V148() V149() set
{{D,j2},{D}} is non empty set
(Gauge (C,n)) * (D,j2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
i4 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j4 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
[i4,j4] is set
{i4,j4} is non empty V144() V145() V146() V147() V148() V149() set
{i4} is non empty V144() V145() V146() V147() V148() V149() set
{{i4,j4},{i4}} is non empty set
(Gauge (C,n)) * (i4,j4) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
j2 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
D + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
i4 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j4 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
right_cell (((Span (C,n)) | p),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
(Span (C,n)) /. (p + 1) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
<*((Span (C,n)) /. (p + 1))*> is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V26() V33(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
((Span (C,n)) | p) ^ <*((Span (C,n)) /. (p + 1))*> is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom ((Span (C,n)) | p) is V144() V145() V146() V147() V148() V149() Element of K6(NAT)
((Span (C,n)) | (p + 1)) /. (i1 + 1) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
left_cell (((Span (C,n)) | p),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
((Span (C,n)) | (p + 1)) /. i1 is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
D -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),(D -' 1),j2) is Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),D,j2) is Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),D,j2) is Element of K6( the carrier of (TOP-REAL 2))
j2 -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),D,(j2 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
j4 -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),i4,(j4 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),i4,j4) is Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),D,j4) is Element of K6( the carrier of (TOP-REAL 2))
i4 -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),(i4 -' 1),j4) is Element of K6( the carrier of (TOP-REAL 2))
(Span (C,n)) | 0 is empty V4() V5() V6() V8() V9() V10() V12() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V21() V26() FinSequence-like FinSubsequence-like FinSequence-membered V37() V144() V145() V146() V147() V148() V149() V150() FinSequence of the carrier of (TOP-REAL 2)
len ((Span (C,n)) | 0) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
p is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
p + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
right_cell (((Span (C,n)) | 0),p,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
left_cell (((Span (C,n)) | 0),p,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
L~ (Span (C,n)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
Gauge (C,n) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
f is set
len (Span (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
{ (LSeg ((Span (C,n)),b1)) where b1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (Span (C,n)) ) } is set
union { (LSeg ((Span (C,n)),b1)) where b1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (Span (C,n)) ) } is set
p is set
i1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
LSeg ((Span (C,n)),i1) is Element of K6( the carrier of (TOP-REAL 2))
i1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
left_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
right_cell ((Span (C,n)),i1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
(left_cell ((Span (C,n)),i1,(Gauge (C,n)))) /\ (right_cell ((Span (C,n)),i1,(Gauge (C,n)))) is Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
RightComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
Cl (RightComp (Span (C,n))) is closed Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
LeftComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
Gauge (C,n) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
len (Span (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
left_cell ((Span (C,n)),1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
L~ (Span (C,n)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
(left_cell ((Span (C,n)),1,(Gauge (C,n)))) \ (L~ (Span (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
RightComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
L~ (Span (C,n)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
(L~ (Span (C,n))) ` is open dense Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | ((L~ (Span (C,n))) `) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)) is set
K6( the carrier of ((TOP-REAL 2) | ((L~ (Span (C,n))) `))) is set
LeftComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
G is set
G is Element of K6( the carrier of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)))
f is Element of K6( the carrier of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)))
p is Element of K6( the carrier of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
LeftComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
m is set
L~ (Span (C,n)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
RightComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
L~ (Span (C,n)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
UBD (L~ (Span (C,n))) is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
LeftComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
BDD C is open Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
L~ (Span (C,n)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Span (C,n))) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
Cl (BDD (L~ (Span (C,n)))) is closed Element of K6( the carrier of (TOP-REAL 2))
RightComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
Cl (RightComp (Span (C,n))) is closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
(RightComp (Span (C,n))) \/ (L~ (Span (C,n))) is non empty Element of K6( the carrier of (TOP-REAL 2))
len (Span (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
dom (Span (C,n)) is V144() V145() V146() V147() V148() V149() Element of K6(NAT)
(Span (C,n)) /. 1 is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(C,n) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
Gauge (C,n) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
X-SpanStart (C,n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Y-SpanStart (C,n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
UBD C is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
UBD (L~ (Span (C,n))) is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
C ` is open Element of K6( the carrier of (TOP-REAL 2))
(BDD C) \/ (UBD C) is non empty open Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
L~ (Span (C,n)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
UBD (L~ (Span (C,n))) is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
m is set
BDD C is open Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Span (C,n))) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
Cl (BDD (L~ (Span (C,n)))) is closed Element of K6( the carrier of (TOP-REAL 2))
Cl (BDD C) is closed Element of K6( the carrier of (TOP-REAL 2))
G is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
RightComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
(RightComp (Span (C,n))) \/ (L~ (Span (C,n))) is non empty Element of K6( the carrier of (TOP-REAL 2))
Cl (RightComp (Span (C,n))) is closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
LeftComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
BDD C is open Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
RightComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
L~ (Span (C,n)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Span (C,n))) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
LeftComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
L~ (Span (C,n)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
UBD (L~ (Span (C,n))) is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
L~ (Span (C,n)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Span (C,n))) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
UBD (L~ (Span (C,n))) is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
RightComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
L~ (Span (C,n)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Span (C,n))) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
n is Element of K6( the carrier of (TOP-REAL 2))
m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,m) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
L~ (Span (C,m)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
LeftComp (Span (C,m)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
G is set
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
L~ (Span (C,n)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
m is set
{ b1 where b1 is Element of K6( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of C } is set
union { b1 where b1 is Element of K6( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of C } is set
G is set
f is Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
BDD C is open Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
L~ (Span (C,n)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
C ` is open Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
(BDD C) \/ (UBD C) is non empty open Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
f is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
G is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,f) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
len (Span (C,f)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
[n,m] is set
{n,m} is non empty V144() V145() V146() V147() V148() V149() set
{n} is non empty V144() V145() V146() V147() V148() V149() set
{{n,m},{n}} is non empty set
Gauge (C,f) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
Indices (Gauge (C,f)) is set
(Span (C,f)) /. G is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,f)) * (n,m) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(C,f) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
X-SpanStart (C,f) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Y-SpanStart (C,f) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Gauge (C,f)) * ((X-SpanStart (C,f)),(Y-SpanStart (C,f))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
BDD C is open Element of K6( the carrier of (TOP-REAL 2))
W-bound C is V11() V12() ext-real Element of REAL
W-bound (BDD C) is V11() V12() ext-real Element of REAL
width (Gauge (C,f)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
dom (Span (C,f)) is V144() V145() V146() V147() V148() V149() Element of K6(NAT)
L~ (Span (C,f)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
W-bound (L~ (Span (C,f))) is V11() V12() ext-real Element of REAL
((Gauge (C,f)) * (n,m)) `1 is V11() V12() ext-real Element of REAL
Cl (BDD C) is closed Element of K6( the carrier of (TOP-REAL 2))
W-bound (Cl (BDD C)) is V11() V12() ext-real Element of REAL
len (Gauge (C,f)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Gauge (C,f)) * (2,m) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((Gauge (C,f)) * (2,m)) `1 is V11() V12() ext-real Element of REAL
1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
f is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
G is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,f) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
len (Span (C,f)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
[n,m] is set
{n,m} is non empty V144() V145() V146() V147() V148() V149() set
{n} is non empty V144() V145() V146() V147() V148() V149() set
{{n,m},{n}} is non empty set
Gauge (C,f) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
Indices (Gauge (C,f)) is set
(Span (C,f)) /. G is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,f)) * (n,m) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
len (Gauge (C,f)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(C,f) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
X-SpanStart (C,f) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Y-SpanStart (C,f) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Gauge (C,f)) * ((X-SpanStart (C,f)),(Y-SpanStart (C,f))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
BDD C is open Element of K6( the carrier of (TOP-REAL 2))
E-bound (BDD C) is V11() V12() ext-real Element of REAL
E-bound C is V11() V12() ext-real Element of REAL
dom (Span (C,f)) is V144() V145() V146() V147() V148() V149() Element of K6(NAT)
L~ (Span (C,f)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
((Gauge (C,f)) * (n,m)) `1 is V11() V12() ext-real Element of REAL
E-bound (L~ (Span (C,f))) is V11() V12() ext-real Element of REAL
Cl (BDD C) is closed Element of K6( the carrier of (TOP-REAL 2))
E-bound (Cl (BDD C)) is V11() V12() ext-real Element of REAL
1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(len (Gauge (C,f))) - 1 is V11() V12() V37() ext-real Element of REAL
0 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(len (Gauge (C,f))) -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
width (Gauge (C,f)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Gauge (C,f)) * (((len (Gauge (C,f))) -' 1),m) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((Gauge (C,f)) * (((len (Gauge (C,f))) -' 1),m)) `1 is V11() V12() ext-real Element of REAL
((len (Gauge (C,f))) -' 1) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
f is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
G is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,f) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
len (Span (C,f)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
[n,m] is set
{n,m} is non empty V144() V145() V146() V147() V148() V149() set
{n} is non empty V144() V145() V146() V147() V148() V149() set
{{n,m},{n}} is non empty set
Gauge (C,f) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
Indices (Gauge (C,f)) is set
(Span (C,f)) /. G is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,f)) * (n,m) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(C,f) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
X-SpanStart (C,f) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Y-SpanStart (C,f) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Gauge (C,f)) * ((X-SpanStart (C,f)),(Y-SpanStart (C,f))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
BDD C is open Element of K6( the carrier of (TOP-REAL 2))
S-bound C is V11() V12() ext-real Element of REAL
S-bound (BDD C) is V11() V12() ext-real Element of REAL
len (Gauge (C,f)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
dom (Span (C,f)) is V144() V145() V146() V147() V148() V149() Element of K6(NAT)
L~ (Span (C,f)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
S-bound (L~ (Span (C,f))) is V11() V12() ext-real Element of REAL
((Gauge (C,f)) * (n,m)) `2 is V11() V12() ext-real Element of REAL
Cl (BDD C) is closed Element of K6( the carrier of (TOP-REAL 2))
S-bound (Cl (BDD C)) is V11() V12() ext-real Element of REAL
width (Gauge (C,f)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Gauge (C,f)) * (n,2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((Gauge (C,f)) * (n,2)) `2 is V11() V12() ext-real Element of REAL
1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
f is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
G is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,f) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
len (Span (C,f)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
[n,m] is set
{n,m} is non empty V144() V145() V146() V147() V148() V149() set
{n} is non empty V144() V145() V146() V147() V148() V149() set
{{n,m},{n}} is non empty set
Gauge (C,f) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
Indices (Gauge (C,f)) is set
(Span (C,f)) /. G is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,f)) * (n,m) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
width (Gauge (C,f)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
dom (Span (C,f)) is V144() V145() V146() V147() V148() V149() Element of K6(NAT)
L~ (Span (C,f)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
((Gauge (C,f)) * (n,m)) `2 is V11() V12() ext-real Element of REAL
N-bound (L~ (Span (C,f))) is V11() V12() ext-real Element of REAL
BDD C is open Element of K6( the carrier of (TOP-REAL 2))
Cl (BDD C) is closed Element of K6( the carrier of (TOP-REAL 2))
(C,f) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
X-SpanStart (C,f) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Y-SpanStart (C,f) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Gauge (C,f)) * ((X-SpanStart (C,f)),(Y-SpanStart (C,f))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
N-bound (BDD C) is V11() V12() ext-real Element of REAL
N-bound (Cl (BDD C)) is V11() V12() ext-real Element of REAL
len (Gauge (C,f)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(len (Gauge (C,f))) - 1 is V11() V12() V37() ext-real Element of REAL
N-bound C is V11() V12() ext-real Element of REAL
(len (Gauge (C,f))) -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Gauge (C,f)) * (n,((len (Gauge (C,f))) -' 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((Gauge (C,f)) * (n,((len (Gauge (C,f))) -' 1))) `2 is V11() V12() ext-real Element of REAL
0 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
((len (Gauge (C,f))) -' 1) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Gauge (C,n) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
width (Gauge (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Y-SpanStart (C,n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
len (Span (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) /. 1 is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
X-SpanStart (C,n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
[(X-SpanStart (C,n)),(Y-SpanStart (C,n))] is set
{(X-SpanStart (C,n)),(Y-SpanStart (C,n))} is non empty V144() V145() V146() V147() V148() V149() set
{(X-SpanStart (C,n))} is non empty V144() V145() V146() V147() V148() V149() set
{{(X-SpanStart (C,n)),(Y-SpanStart (C,n))},{(X-SpanStart (C,n))}} is non empty set
Indices (Gauge (C,n)) is set
C is non empty closed bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
X-SpanStart (C,m) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m -' n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
2 |^ (m -' n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
X-SpanStart (C,n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(X-SpanStart (C,n)) - 2 is V11() V12() V37() ext-real Element of REAL
(2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2) is V11() V12() V37() ext-real Element of REAL
((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2 is V11() V12() V37() ext-real Element of REAL
n -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
2 |^ (n -' 1) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(2 |^ (n -' 1)) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(m -' n) + (n -' 1) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
n - 1 is V11() V12() V37() ext-real Element of REAL
(m -' n) + (n - 1) is V11() V12() V37() ext-real Element of REAL
(m -' n) + n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
((m -' n) + n) - 1 is V11() V12() V37() ext-real Element of REAL
m - 1 is V11() V12() V37() ext-real Element of REAL
m -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
2 |^ (m -' 1) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
C is non empty closed bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Gauge (C,n) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
width (Gauge (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
X-SpanStart (C,n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(X-SpanStart (C,n)) -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
BDD C is open Element of K6( the carrier of (TOP-REAL 2))
G is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),G) is Element of K6( the carrier of (TOP-REAL 2))
X-SpanStart (C,m) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m -' n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
2 |^ (m -' n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(X-SpanStart (C,n)) - 2 is V11() V12() V37() ext-real Element of REAL
(2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2) is V11() V12() V37() ext-real Element of REAL
((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2 is V11() V12() V37() ext-real Element of REAL
len (Gauge (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) is Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
C ` is open Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) is Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
0 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) is Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(0 + 1)) is Element of K6( the carrier of (TOP-REAL 2))
(cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0)) /\ (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(0 + 1))) is Element of K6( the carrier of (TOP-REAL 2))
(Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(0 + 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((X-SpanStart (C,n)) -' 1) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(0 + 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(0 + 1))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(0 + 1)))) is non empty boundary connected convex Element of K6( the carrier of (TOP-REAL 2))
G - 2 is V11() V12() V37() ext-real Element of REAL
(2 |^ (m -' n)) * (G - 2) is V11() V12() V37() ext-real Element of REAL
((2 |^ (m -' n)) * (G - 2)) + 2 is V11() V12() V37() ext-real Element of REAL
2 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
G + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
len (Gauge (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n)))) is Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
(width (Gauge (C,n))) -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
C ` is open Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n)))) is Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
(width (Gauge (C,n))) - 1 is V11() V12() V37() ext-real Element of REAL
((width (Gauge (C,n))) -' 1) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n))))) /\ (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
(Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n)))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((X-SpanStart (C,n)) -' 1) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(width (Gauge (C,n)))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n))))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(width (Gauge (C,n)))))) is non empty boundary connected convex Element of K6( the carrier of (TOP-REAL 2))
len (Gauge (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Gauge (C,m) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
(X-SpanStart (C,m)) -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
i1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),i1) is Element of K6( the carrier of (TOP-REAL 2))
width (Gauge (C,m)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
C is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
len C is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
width C is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
n is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ n is boundary Element of K6( the carrier of (TOP-REAL 2))
m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
G is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell (C,m,G) is Element of K6( the carrier of (TOP-REAL 2))
(cell (C,m,G)) \ (L~ n) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell (C,m,G)) is open Element of K6( the carrier of (TOP-REAL 2))
(L~ n) ` is Element of K6( the carrier of (TOP-REAL 2))
Cl (Int (cell (C,m,G))) is closed Element of K6( the carrier of (TOP-REAL 2))
(cell (C,m,G)) /\ ((L~ n) `) is Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
ApproxIndex C is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Y-InitStart C is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Y-InitStart C) -' 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Y-SpanStart (C,n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
n -' (ApproxIndex C) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
2 |^ (n -' (ApproxIndex C)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Gauge (C,n) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
X-SpanStart (C,n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(X-SpanStart (C,n)) -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),m) is Element of K6( the carrier of (TOP-REAL 2))
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
L~ (Span (C,n)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
(cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),m)) \ (L~ (Span (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Span (C,n))) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
m - (Y-SpanStart (C,n)) is V11() V12() V37() ext-real Element of REAL
i4 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) - (Y-SpanStart (C,n)) is V11() V12() V37() ext-real Element of REAL
(Y-SpanStart (C,n)) + i4 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
((X-SpanStart (C,n)) -' 1) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
len (Gauge (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j4 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Y-SpanStart (C,n)) + j4 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + j4)) is Element of K6( the carrier of (TOP-REAL 2))
(cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + j4))) \ (L~ (Span (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
j4 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Y-SpanStart (C,n)) + (j4 + 1) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (j4 + 1))) is Element of K6( the carrier of (TOP-REAL 2))
(cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (j4 + 1)))) \ (L~ (Span (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
(Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (j4 + 1))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (j4 + 1))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (j4 + 1)))),((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (j4 + 1))))) is non empty boundary connected convex Element of K6( the carrier of (TOP-REAL 2))
((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (j4 + 1)))) + ((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (j4 + 1)))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (j4 + 1)))) + ((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (j4 + 1))))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(L~ (Span (C,n))) ` is open dense Element of K6( the carrier of (TOP-REAL 2))
j4 is set
((Y-SpanStart (C,n)) + j4) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(1 + 1) + 0 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Y-InitStart C) - 2 is V11() V12() V37() ext-real Element of REAL
(j4 + 1) + (Y-SpanStart (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j4 is set
UBD (L~ (Span (C,n))) is non empty open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
(BDD (L~ (Span (C,n)))) \/ (UBD (L~ (Span (C,n)))) is non empty open Element of K6( the carrier of (TOP-REAL 2))
Gauge (C,(ApproxIndex C)) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
width (Gauge (C,(ApproxIndex C))) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
width (Gauge (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) - 2) is V11() V12() V37() ext-real Element of REAL
((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) - 2)) + 2 is V11() V12() V37() ext-real Element of REAL
len (Span (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
LSeg ((Span (C,n)),j) is Element of K6( the carrier of (TOP-REAL 2))
(Span (C,n)) /. j is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Span (C,n)) /. (j + 1) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
LSeg (((Span (C,n)) /. j),((Span (C,n)) /. (j + 1))) is non empty boundary connected convex Element of K6( the carrier of (TOP-REAL 2))
Indices (Gauge (C,n)) is set
f is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j3 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
[f,j3] is set
{f,j3} is non empty V144() V145() V146() V147() V148() V149() set
{f} is non empty V144() V145() V146() V147() V148() V149() set
{{f,j3},{f}} is non empty set
(Gauge (C,n)) * (f,j3) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
p3 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
[p3,j2] is set
{p3,j2} is non empty V144() V145() V146() V147() V148() V149() set
{p3} is non empty V144() V145() V146() V147() V148() V149() set
{{p3,j2},{p3}} is non empty set
(Gauge (C,n)) * (p3,j2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
j3 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
f + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
p3 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j2 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
BDD C is open Element of K6( the carrier of (TOP-REAL 2))
left_cell ((Span (C,n)),j,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),f,j3) is Element of K6( the carrier of (TOP-REAL 2))
left_cell ((Span (C,n)),j,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
j2 -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),p3,(j2 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
((Y-SpanStart (C,n)) + (j4 + 1)) -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(((Y-SpanStart (C,n)) + (j4 + 1)) -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
BDD C is open Element of K6( the carrier of (TOP-REAL 2))
LeftComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
(Y-SpanStart (C,n)) + 0 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + 0)) is Element of K6( the carrier of (TOP-REAL 2))
(cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + 0))) \ (L~ (Span (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,n)) /. (1 + 1) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
[(X-SpanStart (C,n)),(Y-SpanStart (C,n))] is set
{(X-SpanStart (C,n)),(Y-SpanStart (C,n))} is non empty V144() V145() V146() V147() V148() V149() set
{(X-SpanStart (C,n))} is non empty V144() V145() V146() V147() V148() V149() set
{{(X-SpanStart (C,n)),(Y-SpanStart (C,n))},{(X-SpanStart (C,n))}} is non empty set
Indices (Gauge (C,n)) is set
[((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))] is set
{((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))} is non empty V144() V145() V146() V147() V148() V149() set
{((X-SpanStart (C,n)) -' 1)} is non empty V144() V145() V146() V147() V148() V149() set
{{((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))},{((X-SpanStart (C,n)) -' 1)}} is non empty set
len (Span (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
right_cell ((Span (C,n)),1,(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
(right_cell ((Span (C,n)),1,(Gauge (C,n)))) \ (L~ (Span (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
RightComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
(Span (C,n)) /. 1 is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
C is Element of K6( the carrier of (TOP-REAL 2))
m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
G is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Gauge (C,m) is V13() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular FinSequence of K338( the carrier of (TOP-REAL 2))
len (Gauge (C,m)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
G + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Gauge (C,n) is V13() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular FinSequence of K338( the carrier of (TOP-REAL 2))
len (Gauge (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
n -' m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
2 |^ (n -' m) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
G - 2 is V11() V12() V37() ext-real Element of REAL
(2 |^ (n -' m)) * (G - 2) is V11() V12() V37() ext-real Element of REAL
((2 |^ (n -' m)) * (G - 2)) + 2 is V11() V12() V37() ext-real Element of REAL
(((2 |^ (n -' m)) * (G - 2)) + 2) + 1 is V11() V12() V37() ext-real Element of REAL
1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
2 |^ m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
2 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(2 |^ m) + (2 + 1) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(2 |^ m) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
((2 |^ m) + 2) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
f is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(2 |^ (n -' m)) * (2 |^ m) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(2 |^ (n -' m)) * f is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(n -' m) + m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
2 |^ ((n -' m) + m) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
2 |^ n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(2 |^ n) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
((2 |^ (n -' m)) * f) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
((2 |^ n) + 2) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
1 + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(2 |^ n) + (1 + 2) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
RightComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
Span (C,m) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
RightComp (Span (C,m)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
X-SpanStart (C,m) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Gauge (C,m) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
Y-InitStart C is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
ApproxIndex C is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
X-SpanStart (C,n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Gauge (C,n) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
(X-SpanStart (C,m)) -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Y-SpanStart (C,m) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m -' (ApproxIndex C) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
2 |^ (m -' (ApproxIndex C)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Y-InitStart C) -' 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) is Element of K6( the carrier of (TOP-REAL 2))
L~ (Span (C,m)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
(cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) \ (L~ (Span (C,m))) is Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Span (C,m))) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
len (Gauge (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(X-SpanStart (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(len (Gauge (C,n))) - 1 is V11() V12() V37() ext-real Element of REAL
X-SpanStart (C,(ApproxIndex C)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Gauge (C,(ApproxIndex C)) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
(Gauge (C,(ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))),(Y-InitStart C)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
width (Gauge (C,(ApproxIndex C))) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Y-InitStart C) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
n -' (ApproxIndex C) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
2 |^ (n -' (ApproxIndex C)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
len (Gauge (C,m)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Y-SpanStart (C,n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(X-SpanStart (C,n)) -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) is Element of K6( the carrier of (TOP-REAL 2))
L~ (Span (C,n)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
(cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) \ (L~ (Span (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Span (C,n))) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) is open Element of K6( the carrier of (TOP-REAL 2))
((X-SpanStart (C,n)) -' 1) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(1 + 1) + 0 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Y-InitStart C) - 2 is V11() V12() V37() ext-real Element of REAL
(2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) - 2) is V11() V12() V37() ext-real Element of REAL
((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) - 2)) + 2 is V11() V12() V37() ext-real Element of REAL
(2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) - 2) is V11() V12() V37() ext-real Element of REAL
((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) - 2)) + 2 is V11() V12() V37() ext-real Element of REAL
(Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
width (Gauge (C,m)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
((X-SpanStart (C,m)) -' 1) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Int (cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) is open Element of K6( the carrier of (TOP-REAL 2))
((1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))))) `2 is V11() V12() ext-real Element of REAL
((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 is V11() V12() ext-real Element of REAL
(Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 is V11() V12() ext-real Element of REAL
((1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))))) `1 is V11() V12() ext-real Element of REAL
((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `1 is V11() V12() ext-real Element of REAL
(Gauge (C,m)) * ((X-SpanStart (C,m)),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((Gauge (C,m)) * ((X-SpanStart (C,m)),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 is V11() V12() ext-real Element of REAL
(Gauge (C,m)) * (1,(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((Gauge (C,m)) * (1,(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 is V11() V12() ext-real Element of REAL
((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 is V11() V12() ext-real Element of REAL
(Gauge (C,m)) * (1,((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((Gauge (C,m)) * (1,((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 is V11() V12() ext-real Element of REAL
len (Gauge (C,(ApproxIndex C))) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
width (Gauge (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(X-SpanStart (C,(ApproxIndex C))) - 2 is V11() V12() V37() ext-real Element of REAL
(2 |^ (m -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2) is V11() V12() V37() ext-real Element of REAL
((2 |^ (m -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2 is V11() V12() V37() ext-real Element of REAL
(2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2) is V11() V12() V37() ext-real Element of REAL
((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2 is V11() V12() V37() ext-real Element of REAL
(Gauge (C,n)) * ((X-SpanStart (C,n)),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * ((X-SpanStart (C,n)),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 is V11() V12() ext-real Element of REAL
(Gauge (C,n)) * (1,(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * (1,(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 is V11() V12() ext-real Element of REAL
(Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 is V11() V12() ext-real Element of REAL
((Gauge (C,m)) * ((X-SpanStart (C,m)),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `1 is V11() V12() ext-real Element of REAL
((Gauge (C,n)) * ((X-SpanStart (C,n)),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `1 is V11() V12() ext-real Element of REAL
(len (Gauge (C,m))) - 1 is V11() V12() V37() ext-real Element of REAL
Indices (Gauge (C,m)) is set
m -' n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
2 |^ (m -' n) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
((X-SpanStart (C,n)) -' 1) -' 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(2 |^ (m -' n)) * (((X-SpanStart (C,n)) -' 1) -' 2) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
2 + ((2 |^ (m -' n)) * (((X-SpanStart (C,n)) -' 1) -' 2)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) -' 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(2 |^ (m -' n)) * ((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) -' 2) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
2 + ((2 |^ (m -' n)) * ((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) -' 2)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
{ ((Gauge (C,m)) * (b1,b2)) where b1, b2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT : [b1,b2] in Indices (Gauge (C,m)) } is set
j2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
c20 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
[j2,c20] is set
{j2,c20} is non empty V144() V145() V146() V147() V148() V149() set
{j2} is non empty V144() V145() V146() V147() V148() V149() set
{{j2,c20},{j2}} is non empty set
(Gauge (C,m)) * (j2,c20) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
Values (Gauge (C,m)) is Element of K6( the carrier of (TOP-REAL 2))
((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `1 is V11() V12() ext-real Element of REAL
(Gauge (C,n)) * ((X-SpanStart (C,n)),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
(X-SpanStart (C,n)) -' 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(2 |^ (m -' n)) * ((X-SpanStart (C,n)) -' 2) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
2 + ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) -' 2)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1) -' 2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(2 |^ (m -' n)) * (((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1) -' 2) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
2 + ((2 |^ (m -' n)) * (((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1) -' 2)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
c20 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
[j2,c20] is set
{j2,c20} is non empty V144() V145() V146() V147() V148() V149() set
{j2} is non empty V144() V145() V146() V147() V148() V149() set
{{j2,c20},{j2}} is non empty set
(Gauge (C,m)) * (j2,c20) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * ((X-SpanStart (C,n)),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 is V11() V12() ext-real Element of REAL
(Gauge (C,n)) * (1,((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * (1,((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 is V11() V12() ext-real Element of REAL
(Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 is V11() V12() ext-real Element of REAL
C is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
len C is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
width C is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
n is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ n is boundary Element of K6( the carrier of (TOP-REAL 2))
(L~ n) ` is Element of K6( the carrier of (TOP-REAL 2))
m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
G is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell (C,m,G) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell (C,m,G)) is open Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,m) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
L~ (Span (C,m)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
LeftComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
Cl (LeftComp (Span (C,n))) is closed Element of K6( the carrier of (TOP-REAL 2))
Gauge (C,m) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
p is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
len (Span (C,m)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
i1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
i1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
LSeg ((Span (C,m)),i1) is Element of K6( the carrier of (TOP-REAL 2))
Gauge (C,n) is V13() V15() V16( NAT ) V17(K338( the carrier of (TOP-REAL 2))) V18() V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K338( the carrier of (TOP-REAL 2))
len (Gauge (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
width (Gauge (C,n)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
left_cell ((Span (C,m)),i1,(Gauge (C,m))) is Element of K6( the carrier of (TOP-REAL 2))
dom (Span (C,m)) is V144() V145() V146() V147() V148() V149() Element of K6(NAT)
Indices (Gauge (C,m)) is set
(Span (C,m)) /. (i1 + 1) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
D is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
[D,j2] is set
{D,j2} is non empty V144() V145() V146() V147() V148() V149() set
{D} is non empty V144() V145() V146() V147() V148() V149() set
{{D,j2},{D}} is non empty set
(Gauge (C,m)) * (D,j2) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
width (Gauge (C,m)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
len (Gauge (C,m)) is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(Span (C,m)) /. i1 is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
i4 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j4 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
[i4,j4] is set
{i4,j4} is non empty V144() V145() V146() V147() V148() V149() set
{i4} is non empty V144() V145() V146() V147() V148() V149() set
{{i4,j4},{i4}} is non empty set
(Gauge (C,m)) * (i4,j4) is V33(2) FinSequence-like V136() Element of the carrier of (TOP-REAL 2)
i4 - D is V11() V12() V37() ext-real Element of REAL
abs (i4 - D) is V11() V12() ext-real Element of REAL
j4 - j2 is V11() V12() V37() ext-real Element of REAL
abs (j4 - j2) is V11() V12() ext-real Element of REAL
(abs (i4 - D)) + (abs (j4 - j2)) is V11() V12() ext-real Element of REAL
j4 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
i4 -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,m)),(i4 -' 1),j4) is Element of K6( the carrier of (TOP-REAL 2))
i4 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,m)),i4,j4) is Element of K6( the carrier of (TOP-REAL 2))
D + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j2 -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,m)),D,(j2 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
j2 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,m)),i4,j2) is Element of K6( the carrier of (TOP-REAL 2))
1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(i4 -' 1) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
(j2 -' 1) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
D is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
D + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j2 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),D,j2) is Element of K6( the carrier of (TOP-REAL 2))
D is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
D + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j2 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
j2 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
cell ((Gauge (C,n)),D,j2) is Element of K6( the carrier of (TOP-REAL 2))
L~ (Span (C,n)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
(L~ (Span (C,n))) ` is open dense Element of K6( the carrier of (TOP-REAL 2))
RightComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
Cl (RightComp (Span (C,n))) is closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
(Cl (RightComp (Span (C,n)))) \/ (LeftComp (Span (C,n))) is Element of K6( the carrier of (TOP-REAL 2))
(L~ (Span (C,n))) \/ (RightComp (Span (C,n))) is non empty Element of K6( the carrier of (TOP-REAL 2))
((L~ (Span (C,n))) \/ (RightComp (Span (C,n)))) \/ (LeftComp (Span (C,n))) is non empty Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((Gauge (C,n)),D,j2)) is open Element of K6( the carrier of (TOP-REAL 2))
Cl (Int (cell ((Gauge (C,n)),D,j2))) is closed Element of K6( the carrier of (TOP-REAL 2))
Int (left_cell ((Span (C,m)),i1,(Gauge (C,m)))) is open Element of K6( the carrier of (TOP-REAL 2))
Cl (Int (left_cell ((Span (C,m)),i1,(Gauge (C,m))))) is closed Element of K6( the carrier of (TOP-REAL 2))
(RightComp (Span (C,n))) \/ (L~ (Span (C,n))) is non empty Element of K6( the carrier of (TOP-REAL 2))
D is Element of K6( the carrier of (TOP-REAL 2))
(RightComp (Span (C,n))) \/ (LeftComp (Span (C,n))) is open Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
RightComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
Span (C,m) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
RightComp (Span (C,m)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
L~ (Span (C,n)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
LeftComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
Cl (LeftComp (Span (C,n))) is closed Element of K6( the carrier of (TOP-REAL 2))
(LeftComp (Span (C,n))) \/ (L~ (Span (C,n))) is non empty Element of K6( the carrier of (TOP-REAL 2))
L~ (Span (C,m)) is non empty closed boundary nowhere_dense connected bounded V175() compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
(L~ (Span (C,m))) ` is open dense Element of K6( the carrier of (TOP-REAL 2))
C is non empty closed connected bounded compact non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
n is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
m is V4() V5() V6() V10() V11() V12() V37() ext-real V97() V144() V145() V146() V147() V148() V149() Element of NAT
Span (C,m) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
LeftComp (Span (C,m)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
Span (C,n) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) V18() non constant V26() FinSequence-like FinSubsequence-like V180( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V194() FinSequence of the carrier of (TOP-REAL 2)
LeftComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
RightComp (Span (C,n)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
Cl (RightComp (Span (C,n))) is closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
(Cl (RightComp (Span (C,n)))) ` is open Element of K6( the carrier of (TOP-REAL 2))
RightComp (Span (C,m)) is open connected V174( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
Cl (RightComp (Span (C,m))) is closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
(Cl (RightComp (Span (C,m)))) ` is open Element of K6( the carrier of (TOP-REAL 2))