:: GOBOARD3 semantic presentation

REAL is set

NAT is non empty V4() V5() V6() V33() V38() V39() Element of bool REAL

bool REAL is set

COMPLEX is set

NAT is non empty V4() V5() V6() V33() V38() V39() set

bool NAT is V33() set

bool NAT is V33() set

1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

[:1,1:] is set

bool [:1,1:] is set

[:[:1,1:],1:] is set

bool [:[:1,1:],1:] is set

[:[:1,1:],REAL:] is set

bool [:[:1,1:],REAL:] is set

[:REAL,REAL:] is set

[:[:REAL,REAL:],REAL:] is set

bool [:[:REAL,REAL:],REAL:] is set

2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

[:2,2:] is set

[:[:2,2:],REAL:] is set

bool [:[:2,2:],REAL:] is set

RAT is set

INT is set

bool [:REAL,REAL:] is set

TOP-REAL 2 is non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() strict RLTopStruct

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

bool the U1 of (TOP-REAL 2) is set

K292( the U1 of (TOP-REAL 2)) is non empty functional FinSequence-membered M11( the U1 of (TOP-REAL 2))

{} is set

the empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative functional V33() V38() V40( {} ) FinSequence-membered V71() set is empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative functional V33() V38() V40( {} ) FinSequence-membered V71() set

3 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

Seg 1 is non empty trivial V33() V40(1) Element of bool NAT

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

Seg 2 is non empty V33() V40(2) Element of bool NAT

{1,2} is set

0 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

G is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

f is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

f | G is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

dom (f | G) is Element of bool NAT

len (f | G) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

Seg (len (f | G)) is V33() V40( len (f | G)) Element of bool NAT

len f is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

G + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

0 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

dom f is Element of bool NAT

g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set

g + 2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

LSeg ((f | G),g) is Element of bool the U1 of (TOP-REAL 2)

g + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

LSeg ((f | G),(g + 1)) is Element of bool the U1 of (TOP-REAL 2)

(LSeg ((f | G),g)) /\ (LSeg ((f | G),(g + 1))) is Element of bool the U1 of (TOP-REAL 2)

(f | G) /. (g + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

{((f | G) /. (g + 1))} is non empty trivial V40(1) set

f1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

f1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

LSeg ((f | G),f1) is Element of bool the U1 of (TOP-REAL 2)

LSeg (f,f1) is Element of bool the U1 of (TOP-REAL 2)

f1 + 2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

(f1 + 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

f1 + (1 + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

LSeg ((f | G),(f1 + 1)) is Element of bool the U1 of (TOP-REAL 2)

LSeg (f,(f1 + 1)) is Element of bool the U1 of (TOP-REAL 2)

(f | G) /. (f1 + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

f /. (f1 + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

f is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

dom f is Element of bool NAT

L~ f is Element of bool the U1 of (TOP-REAL 2)

len f is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

{ (LSeg (f,b

union { (LSeg (f,b

f /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

f /. (len f) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

G is V16() non empty-yielding V19( NAT ) V20(K292( the U1 of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K292( the U1 of (TOP-REAL 2))

Indices G is set

g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

g + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

c

len c

dom c

L~ c

{ (LSeg (c

union { (LSeg (c

c

c

f1 is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

L~ f1 is Element of bool the U1 of (TOP-REAL 2)

len f1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

{ (LSeg (f1,b

union { (LSeg (f1,b

f1 /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

f1 /. (len f1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

j1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

dom f1 is Element of bool NAT

j1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

f1 /. j1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

f1 /. (j1 + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

j2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

i1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

[j2,i1] is set

{j2,i1} is set

{j2} is non empty trivial V40(1) set

{{j2,i1},{j2}} is set

i2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

l1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

[i2,l1] is set

{i2,l1} is set

{i2} is non empty trivial V40(1) set

{{i2,l1},{i2}} is set

G * (j2,i1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

G * (i2,l1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

j2 - i2 is V11() V12() ext-real V71() set

abs (j2 - i2) is V11() V12() ext-real Element of REAL

i1 - l1 is V11() V12() ext-real V71() set

abs (i1 - l1) is V11() V12() ext-real Element of REAL

(abs (j2 - i2)) + (abs (i1 - l1)) is V11() V12() ext-real set

c

len (c

Seg g is V33() V40(g) Element of bool NAT

c

[:NAT, the U1 of (TOP-REAL 2):] is V33() set

bool [:NAT, the U1 of (TOP-REAL 2):] is V33() set

dom G is Element of bool NAT

len G is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

Seg (len G) is V33() V40( len G) Element of bool NAT

c

j1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

j2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

[j1,j2] is set

{j1,j2} is set

{j1} is non empty trivial V40(1) set

{{j1,j2},{j1}} is set

G * (j1,j2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

width G is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

Seg (width G) is V33() V40( width G) Element of bool NAT

[:(dom G),(Seg (width G)):] is set

c

i1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

i2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

[i1,i2] is set

{i1,i2} is set

{i1} is non empty trivial V40(1) set

{{i1,i2},{i1}} is set

G * (i1,i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

Line (G,i1) is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like M12( the U1 of (TOP-REAL 2),K293((width G), the U1 of (TOP-REAL 2)))

K293((width G), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M11( the U1 of (TOP-REAL 2))

Col (G,i2) is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like M12( the U1 of (TOP-REAL 2),K293((len G), the U1 of (TOP-REAL 2)))

K293((len G), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M11( the U1 of (TOP-REAL 2))

l1 is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

X_axis l1 is V16() V19( NAT ) V20( REAL ) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of REAL

Y_axis l1 is V16() V19( NAT ) V20( REAL ) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of REAL

c1 is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

X_axis c1 is V16() V19( NAT ) V20( REAL ) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of REAL

Y_axis c1 is V16() V19( NAT ) V20( REAL ) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of REAL

dom (Y_axis l1) is Element of bool NAT

len (Y_axis l1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

Seg (len (Y_axis l1)) is V33() V40( len (Y_axis l1)) Element of bool NAT

len l1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

dom (c

Seg (len (c

g1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set

g1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

(c

((c

(c

((c

((c

((c

c

c

g1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

c

ppi is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

pj is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

[ppi,pj] is set

{ppi,pj} is set

{ppi} is non empty trivial V40(1) set

{{ppi,pj},{ppi}} is set

G * (ppi,pj) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

l is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

g2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

[l,g2] is set

{l,g2} is set

{l} is non empty trivial V40(1) set

{{l,g2},{l}} is set

(c

G * (l,g2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

L~ (c

{ (LSeg ((c

union { (LSeg ((c

(c

(c

g1 is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

L~ g1 is Element of bool the U1 of (TOP-REAL 2)

len g1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

{ (LSeg (g1,b

union { (LSeg (g1,b

g1 /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

g1 /. (len g1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

dom g1 is Element of bool NAT

ppi is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

ppi + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

pj is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

l is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

[pj,l] is set

{pj,l} is set

{pj} is non empty trivial V40(1) set

{{pj,l},{pj}} is set

g2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

[g2,g] is set

{g2,g} is set

{g2} is non empty trivial V40(1) set

{{g2,g},{g2}} is set

g1 /. ppi is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

G * (pj,l) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

g1 /. (ppi + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

G * (g2,g) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

pj - g2 is V11() V12() ext-real V71() set

abs (pj - g2) is V11() V12() ext-real Element of REAL

l - g is V11() V12() ext-real V71() set

abs (l - g) is V11() V12() ext-real Element of REAL

(abs (pj - g2)) + (abs (l - g)) is V11() V12() ext-real set

rng g1 is set

1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

ppi is set

pj is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

g1 /. pj is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

{(c

ppi is set

pj is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

g1 /. pj is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

Seg (len g1) is V33() V40( len g1) Element of bool NAT

len c1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

dom c1 is Element of bool NAT

dom (Y_axis c1) is Element of bool NAT

len (Y_axis c1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

Seg (len (Y_axis c1)) is V33() V40( len (Y_axis c1)) Element of bool NAT

dom (X_axis l1) is Element of bool NAT

len (X_axis l1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

Seg (len (X_axis l1)) is V33() V40( len (X_axis l1)) Element of bool NAT

dom (X_axis c1) is Element of bool NAT

len (X_axis c1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

Seg (len (X_axis c1)) is V33() V40( len (X_axis c1)) Element of bool NAT

dom l1 is Element of bool NAT

ppi is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

g1 /. ppi is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

G * (i1,j2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

l1 /. i2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

l1 . i2 is set

(Y_axis l1) . i2 is set

(G * (i1,i2)) `2 is V11() V12() ext-real Element of REAL

l1 /. j2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

l1 . j2 is set

(Y_axis l1) . j2 is set

(G * (i1,j2)) `2 is V11() V12() ext-real Element of REAL

i2 - j2 is V11() V12() ext-real V71() set

(G * (i1,i2)) `1 is V11() V12() ext-real Element of REAL

{ b

|[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

l is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

Seg l is V33() V40(l) Element of bool NAT

i2 - g is V11() V12() ext-real V71() set

lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

i2 - l is V11() V12() ext-real V71() set

[i1,(i2 - g)] is set

{i1,(i2 - g)} is set

{{i1,(i2 - g)},{i1}} is set

g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set

i2 - g is V11() V12() ext-real V71() set

lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

G * (i1,lk) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

G * (i1,lf) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

g is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

len g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

g1 ^ g is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

dom g is Element of bool NAT

lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

i2 - lg is V11() V12() ext-real V71() set

lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

[x,p1] is set

{x,p1} is set

{x} is non empty trivial V40(1) set

{{x,p1},{x}} is set

g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

G * (x,p1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lk is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

dom lk is Element of bool NAT

lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

lk /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

Seg (len g) is V33() V40( len g) Element of bool NAT

(X_axis l1) . i2 is set

lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

i2 - lg is V11() V12() ext-real V71() set

i2 - (len g) is V11() V12() ext-real V71() set

x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

G * (i1,x) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

(X_axis l1) . x is set

l1 /. x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

l1 . x is set

(Y_axis l1) . x is set

(G * (i1,x)) `2 is V11() V12() ext-real Element of REAL

(G * (i1,x)) `1 is V11() V12() ext-real Element of REAL

lf `1 is V11() V12() ext-real Element of REAL

lf `2 is V11() V12() ext-real Element of REAL

Seg (len l1) is V33() V40( len l1) Element of bool NAT

rng l1 is set

lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set

lg + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

(g /. lg) `1 is V11() V12() ext-real Element of REAL

g /. (lg + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

(g /. (lg + 1)) `1 is V11() V12() ext-real Element of REAL

(g /. lg) `2 is V11() V12() ext-real Element of REAL

(g /. (lg + 1)) `2 is V11() V12() ext-real Element of REAL

lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

i2 - lg is V11() V12() ext-real V71() set

i2 - lf is V11() V12() ext-real V71() set

ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

G * (i1,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

G * (i1,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

l1 /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

l1 . ma is set

(Y_axis l1) . ma is set

(G * (i1,ma)) `2 is V11() V12() ext-real Element of REAL

l1 /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

l1 . ma is set

(Y_axis l1) . ma is set

(G * (i1,ma)) `2 is V11() V12() ext-real Element of REAL

x `2 is V11() V12() ext-real Element of REAL

p1 `2 is V11() V12() ext-real Element of REAL

lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

lg + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

LSeg (g,lg) is Element of bool the U1 of (TOP-REAL 2)

lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

LSeg (g,lf) is Element of bool the U1 of (TOP-REAL 2)

(LSeg (g,lg)) /\ (LSeg (g,lf)) is Element of bool the U1 of (TOP-REAL 2)

g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

g /. (lg + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

g /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

x `1 is V11() V12() ext-real Element of REAL

p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

p1 `1 is V11() V12() ext-real Element of REAL

x `2 is V11() V12() ext-real Element of REAL

p1 `2 is V11() V12() ext-real Element of REAL

{ b

ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

ma `2 is V11() V12() ext-real Element of REAL

ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

ma `2 is V11() V12() ext-real Element of REAL

{ b

|[(x `1),(x `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

|[(p1 `1),(p1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

ma `1 is V11() V12() ext-real Element of REAL

|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

ma `1 is V11() V12() ext-real Element of REAL

|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

the Element of (LSeg (g,lg)) /\ (LSeg (g,lf)) is Element of (LSeg (g,lg)) /\ (LSeg (g,lf))

LSeg (ma,ma) is Element of bool the U1 of (TOP-REAL 2)

LSeg (p1,x) is Element of bool the U1 of (TOP-REAL 2)

q2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

q2 `1 is V11() V12() ext-real Element of REAL

q2 `2 is V11() V12() ext-real Element of REAL

x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

x `1 is V11() V12() ext-real Element of REAL

x `2 is V11() V12() ext-real Element of REAL

L~ g is Element of bool the U1 of (TOP-REAL 2)

{ (LSeg (g,b

union { (LSeg (g,b

lf is set

x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

LSeg (g,x) is Element of bool the U1 of (TOP-REAL 2)

x + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

g /. x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

g /. (x + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

p1 `1 is V11() V12() ext-real Element of REAL

ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

ma `2 is V11() V12() ext-real Element of REAL

p1 `2 is V11() V12() ext-real Element of REAL

{ b

|[(p1 `1),(p1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

ma `1 is V11() V12() ext-real Element of REAL

|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

LSeg (ma,p1) is Element of bool the U1 of (TOP-REAL 2)

qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

qa `1 is V11() V12() ext-real Element of REAL

qa `2 is V11() V12() ext-real Element of REAL

(X_axis l1) . j2 is set

(G * (i1,j2)) `1 is V11() V12() ext-real Element of REAL

lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

i2 - lg is V11() V12() ext-real V71() set

i2 - lf is V11() V12() ext-real V71() set

g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

G * (i1,x) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

G * (i1,p1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

[i1,(i2 - lg)] is set

{i1,(i2 - lg)} is set

{{i1,(i2 - lg)},{i1}} is set

[i1,(i2 - lf)] is set

{i1,(i2 - lf)} is set

{{i1,(i2 - lf)},{i1}} is set

lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

|[((G * (i1,j2)) `1),((G * (i1,j2)) `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

LSeg (c

LSeg ((G * (i1,j2)),(G * (i1,i2))) is Element of bool the U1 of (TOP-REAL 2)

rng g is set

lf is set

x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

g /. x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

i2 - x is V11() V12() ext-real V71() set

p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

G * (i1,p1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

(G * (i1,p1)) `2 is V11() V12() ext-real Element of REAL

(G * (i1,p1)) `1 is V11() V12() ext-real Element of REAL

lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

i2 - lf is V11() V12() ext-real V71() set

i2 - (lf + 1) is V11() V12() ext-real V71() set

ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

[ma,ma] is set

{ma,ma} is set

{ma} is non empty trivial V40(1) set

{{ma,ma},{ma}} is set

qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

qa1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

[qa,qa1] is set

{qa,qa1} is set

{qa} is non empty trivial V40(1) set

{{qa,qa1},{qa}} is set

g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

G * (ma,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

g /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

G * (qa,qa1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

[i1,(i2 - (lf + 1))] is set

{i1,(i2 - (lf + 1))} is set

{{i1,(i2 - (lf + 1))},{i1}} is set

p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

G * (i1,p1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

[i1,(i2 - lf)] is set

{i1,(i2 - lf)} is set

{{i1,(i2 - lf)},{i1}} is set

x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

G * (i1,x) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

ma - qa is V11() V12() ext-real V71() set

abs (ma - qa) is V11() V12() ext-real Element of REAL

ma - qa1 is V11() V12() ext-real V71() set

abs (ma - qa1) is V11() V12() ext-real Element of REAL

(abs (ma - qa)) + (abs (ma - qa1)) is V11() V12() ext-real set

(i2 - lf) - (i2 - (lf + 1)) is V11() V12() ext-real V71() set

abs ((i2 - lf) - (i2 - (lf + 1))) is V11() V12() ext-real Element of REAL

0 + (abs ((i2 - lf) - (i2 - (lf + 1)))) is V11() V12() ext-real set

lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

[lf,x] is set

{lf,x} is set

{lf} is non empty trivial V40(1) set

{{lf,x},{lf}} is set

p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

[p1,ma] is set

{p1,ma} is set

{p1} is non empty trivial V40(1) set

{{p1,ma},{p1}} is set

G * (lf,x) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

g /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

G * (p1,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

i2 - 1 is V11() V12() ext-real V71() set

[i1,(i2 - 1)] is set

{i1,(i2 - 1)} is set

{{i1,(i2 - 1)},{i1}} is set

ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

G * (i1,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lf - p1 is V11() V12() ext-real V71() set

abs (lf - p1) is V11() V12() ext-real Element of REAL

x - ma is V11() V12() ext-real V71() set

abs (x - ma) is V11() V12() ext-real Element of REAL

(abs (lf - p1)) + (abs (x - ma)) is V11() V12() ext-real set

i2 - (i2 - 1) is V11() V12() ext-real V71() set

abs (i2 - (i2 - 1)) is V11() V12() ext-real Element of REAL

0 + (abs (i2 - (i2 - 1))) is V11() V12() ext-real set

lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

[x,p1] is set

{x,p1} is set

{x} is non empty trivial V40(1) set

{{x,p1},{x}} is set

ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

[ma,ma] is set

{ma,ma} is set

{ma} is non empty trivial V40(1) set

{{ma,ma},{ma}} is set

lk /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

G * (x,p1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lk /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

G * (ma,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

x - ma is V11() V12() ext-real V71() set

abs (x - ma) is V11() V12() ext-real Element of REAL

p1 - ma is V11() V12() ext-real V71() set

abs (p1 - ma) is V11() V12() ext-real Element of REAL

(abs (x - ma)) + (abs (p1 - ma)) is V11() V12() ext-real set

LSeg ((G * (i1,i2)),(G * (i1,j2))) is Element of bool the U1 of (TOP-REAL 2)

lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

i2 - lf is V11() V12() ext-real V71() set

[i1,(i2 - lf)] is set

{i1,(i2 - lf)} is set

{{i1,(i2 - lf)},{i1}} is set

x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

G * (i1,x) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

(rng g1) /\ (rng g) is set

the Element of (rng g1) /\ (rng g) is Element of (rng g1) /\ (rng g)

(L~ (c

lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

lf + 2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

LSeg (g,lf) is Element of bool the U1 of (TOP-REAL 2)

lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

LSeg (g,(lf + 1)) is Element of bool the U1 of (TOP-REAL 2)

(LSeg (g,lf)) /\ (LSeg (g,(lf + 1))) is Element of bool the U1 of (TOP-REAL 2)

g /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

{(g /. (lf + 1))} is non empty trivial V40(1) set

x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

x `1 is V11() V12() ext-real Element of REAL

x `2 is V11() V12() ext-real Element of REAL

g /. (lf + 2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

p1 `1 is V11() V12() ext-real Element of REAL

p1 `2 is V11() V12() ext-real Element of REAL

1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

lf + (1 + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

(lf + 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

LSeg (x,p1) is Element of bool the U1 of (TOP-REAL 2)

g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

ma `1 is V11() V12() ext-real Element of REAL

ma `2 is V11() V12() ext-real Element of REAL

LSeg (ma,x) is Element of bool the U1 of (TOP-REAL 2)

{ b

|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

|[(p1 `1),(p1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

LSeg ((g /. lf),(g /. (lf + 2))) is Element of bool the U1 of (TOP-REAL 2)

lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set

lf + 2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

len lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

LSeg (lk,lf) is Element of bool the U1 of (TOP-REAL 2)

lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

LSeg (lk,(lf + 1)) is Element of bool the U1 of (TOP-REAL 2)

(LSeg (lk,lf)) /\ (LSeg (lk,(lf + 1))) is Element of bool the U1 of (TOP-REAL 2)

lk /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

{(lk /. (lf + 1))} is non empty trivial V40(1) set

(lf + 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

lf + (1 + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

(len g1) + (len g) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

(lf + 2) - (len g1) is V11() V12() ext-real V71() set

lf - (len g1) is V11() V12() ext-real V71() set

(lf - (len g1)) + 2 is V11() V12() ext-real V71() set

g1 /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

LSeg (g1,lf) is Element of bool the U1 of (TOP-REAL 2)

LSeg (g1,(lf + 1)) is Element of bool the U1 of (TOP-REAL 2)

(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

(lf + 2) - 1 is V11() V12() ext-real V71() set

(L~ (c

(len lk) - (len g1) is V11() V12() ext-real V71() set

x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

x `1 is V11() V12() ext-real Element of REAL

x `2 is V11() V12() ext-real Element of REAL

LSeg ((G * (i1,i2)),x) is Element of bool the U1 of (TOP-REAL 2)

LSeg (g1,lf) is Element of bool the U1 of (TOP-REAL 2)

lk /. (lf + 2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

0 + 2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

p1 `1 is V11() V12() ext-real Element of REAL

p1 `2 is V11() V12() ext-real Element of REAL

g /. 2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

ma `1 is V11() V12() ext-real Element of REAL

ma `2 is V11() V12() ext-real Element of REAL

{ b

|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

LSeg ((G * (i1,i2)),(g /. 2)) is Element of bool the U1 of (TOP-REAL 2)

lk /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

LSeg ((G * (i1,i2)),p1) is Element of bool the U1 of (TOP-REAL 2)

lk /. (lf + 2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

LSeg (p1,ma) is Element of bool the U1 of (TOP-REAL 2)

x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

x + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

LSeg (g,x) is Element of bool the U1 of (TOP-REAL 2)

x + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

(x + 1) + (len g1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

g /. (x + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

LSeg (g,(x + 1)) is Element of bool the U1 of (TOP-REAL 2)

lf is set

p1 is set

ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

LSeg (g,ma) is Element of bool the U1 of (TOP-REAL 2)

ma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

g /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

g /. (ma + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

LSeg (ma,qa) is Element of bool the U1 of (TOP-REAL 2)

(L~ g1) /\ (L~ g) is Element of bool the U1 of (TOP-REAL 2)

(L~ g1) /\ (LSeg (c

the Element of (L~ g1) /\ (L~ g) is Element of (L~ g1) /\ (L~ g)

lk /. (len g1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

ma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

LSeg (lk,ma) is Element of bool the U1 of (TOP-REAL 2)

ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

ma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

LSeg (lk,ma) is Element of bool the U1 of (TOP-REAL 2)

j2 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lf `1 is V11() V12() ext-real Element of REAL

lf `2 is V11() V12() ext-real Element of REAL

(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

lk /. ((len g1) + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

len lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

|[(lf `1),(lf `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

{ b

(len g1) + (len g) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

LSeg (lk,(len g1)) is Element of bool the U1 of (TOP-REAL 2)

LSeg (lf,(G * (i1,i2))) is Element of bool the U1 of (TOP-REAL 2)

LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)

LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)

ma - (len g1) is V11() V12() ext-real V71() set

lma is set

q2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

q2 `1 is V11() V12() ext-real Element of REAL

q2 `2 is V11() V12() ext-real Element of REAL

1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

(L~ (c

LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)

(LSeg (lk,ma)) /\ (LSeg (lk,ma)) is Element of bool the U1 of (TOP-REAL 2)

the Element of (LSeg (lk,ma)) /\ (LSeg (lk,ma)) is Element of (LSeg (lk,ma)) /\ (LSeg (lk,ma))

qa1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

qa1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

(qa1 + 1) + (len g1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

qa1 + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

LSeg (g,qa1) is Element of bool the U1 of (TOP-REAL 2)

LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)

(LSeg (lk,ma)) /\ (LSeg (lk,ma)) is Element of bool the U1 of (TOP-REAL 2)

ma - (len g1) is V11() V12() ext-real V71() set

(ma - (len g1)) + 1 is V11() V12() ext-real V71() set

(ma + 1) - (len g1) is V11() V12() ext-real V71() set

lma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

lma + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

g /. qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

g /. (qa1 + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

(LSeg (lk,ma)) /\ (LSeg (lk,ma)) is Element of bool the U1 of (TOP-REAL 2)

the Element of (LSeg (lk,ma)) /\ (LSeg (lk,ma)) is Element of (LSeg (lk,ma)) /\ (LSeg (lk,ma))

x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

x `2 is V11() V12() ext-real Element of REAL

q2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

q2 `2 is V11() V12() ext-real Element of REAL

{ b

q2 `1 is V11() V12() ext-real Element of REAL

|[(q2 `1),(q2 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

x `1 is V11() V12() ext-real Element of REAL

|[(x `1),(x `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

LSeg (x,q2) is Element of bool the U1 of (TOP-REAL 2)

lma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

c

c

c

c

c

c

LSeg (g,lma) is Element of bool the U1 of (TOP-REAL 2)

lma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

j2 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

(g /. 1) `1 is V11() V12() ext-real Element of REAL

(g1 /. (len g1)) `1 is V11() V12() ext-real Element of REAL

(g1 /. (len g1)) `2 is V11() V12() ext-real Element of REAL

(g /. 1) `2 is V11() V12() ext-real Element of REAL

L~ lk is Element of bool the U1 of (TOP-REAL 2)

len lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

{ (LSeg (lk,b

union { (LSeg (lk,b

(len g1) + (len g) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

p1 - (len g1) is V11() V12() ext-real V71() set

ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lk /. p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lk /. (len g1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

ma `1 is V11() V12() ext-real Element of REAL

ma `2 is V11() V12() ext-real Element of REAL

(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

ma + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

g /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

ma `1 is V11() V12() ext-real Element of REAL

ma `2 is V11() V12() ext-real Element of REAL

ma `1 is V11() V12() ext-real Element of REAL

ma `2 is V11() V12() ext-real Element of REAL

ma `1 is V11() V12() ext-real Element of REAL

ma `2 is V11() V12() ext-real Element of REAL

p1 is set

ma is set

ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

LSeg (lk,ma) is Element of bool the U1 of (TOP-REAL 2)

ma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)

lk /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lk /. (ma + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

qa `1 is V11() V12() ext-real Element of REAL

qa `2 is V11() V12() ext-real Element of REAL

qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

qa1 `1 is V11() V12() ext-real Element of REAL

qa1 `2 is V11() V12() ext-real Element of REAL

|[(qa `1),(qa1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

|[(qa `1),(qa `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

LSeg (qa1,qa) is Element of bool the U1 of (TOP-REAL 2)

{ b

lma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lma `1 is V11() V12() ext-real Element of REAL

lma `2 is V11() V12() ext-real Element of REAL

{qa} is non empty trivial V40(1) set

{ b

lma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lma `1 is V11() V12() ext-real Element of REAL

lma `2 is V11() V12() ext-real Element of REAL

p1 is set

(L~ (c

ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

ma `1 is V11() V12() ext-real Element of REAL

ma `2 is V11() V12() ext-real Element of REAL

ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set

qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set

lk /. qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

qa1 `2 is V11() V12() ext-real Element of REAL

ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set

lk /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set

lk /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

qa - 1 is V11() V12() ext-real V71() set

qa1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

lk /. qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lma `1 is V11() V12() ext-real Element of REAL

lma `2 is V11() V12() ext-real Element of REAL

{ b

lk /. qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

g /. l is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

qa1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

|[(lma `1),(lma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

LSeg (lk,qa1) is Element of bool the U1 of (TOP-REAL 2)

LSeg ((G * (i1,j2)),lma) is Element of bool the U1 of (TOP-REAL 2)

qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

qa + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT

lk /. qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lk /. (qa + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lma `2 is V11() V12() ext-real Element of REAL

qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

qa1 `2 is V11() V12() ext-real Element of REAL

{ b

lma `1 is V11() V12() ext-real Element of REAL

|[(lma `1),(lma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

x `2 is V11() V12() ext-real Element of REAL

qa1 `1 is V11() V12() ext-real Element of REAL

|[(qa1 `1),(qa1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)

LSeg (lk,qa) is Element of bool the U1 of (TOP-REAL 2)

LSeg (lma,qa1) is Element of bool the U1 of (TOP-REAL 2)

qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

(len g1) + (len g) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

lk /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lk /. (len lk) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

g /. l is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

G * (i1,lg) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

l1 /. i2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

l1 . i2 is set

(Y_axis l1) . i2 is set

(G * (i1,i2)) `2 is V11() V12() ext-real Element of REAL

l1 /. j2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

l1 . j2 is set

(Y_axis l1) . j2 is set

(G * (i1,j2)) `2 is V11() V12() ext-real Element of REAL

j2 - i2 is V11() V12() ext-real V71() set

l is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

g2 is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

len g2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

dom g2 is Element of bool NAT

g1 ^ g2 is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

Seg (len g2) is V33() V40( len g2) Element of bool NAT

lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

i2 + lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

Seg l is V33() V40(l) Element of bool NAT

l + i2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

[i1,(i2 + lk)] is set

{i1,(i2 + lk)} is set

{{i1,(i2 + lk)},{i1}} is set

lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

i2 + lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT

[lg,lf] is set

{lg,lf} is set

{lg} is non empty trivial V40(1) set

{{lg,lf},{lg}} is set

g2 /. lk is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

G * (lg,lf) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)

g is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like