:: JORDAN1H semantic presentation

REAL is non empty non trivial non finite non empty-membered V69() V70() V71() V75() set

NAT is non empty non trivial ordinal non finite cardinal limit_cardinal non empty-membered V69() V70() V71() V72() V73() V74() V75() Element of bool REAL

bool REAL is non empty non trivial non finite non empty-membered set

COMPLEX is non empty non trivial non finite non empty-membered V69() V75() set

omega is non empty non trivial ordinal non finite cardinal limit_cardinal non empty-membered V69() V70() V71() V72() V73() V74() V75() set

bool omega is non empty non trivial non finite non empty-membered set

bool NAT is non empty non trivial non finite non empty-membered set

RAT is non empty non trivial non finite non empty-membered V69() V70() V71() V72() V75() set

INT is non empty non trivial non finite non empty-membered V69() V70() V71() V72() V73() V75() set

[:REAL,REAL:] is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set

bool [:REAL,REAL:] is non empty non trivial non finite non empty-membered set

{} is set

the empty ordinal natural V11() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() Function-yielding V81() FinSequence-yielding finite-support set is empty ordinal natural V11() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() Function-yielding V81() FinSequence-yielding finite-support set

1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

{{},1} is finite set

K386() is set

bool K386() is set

K387() is Element of bool K386()

[:1,1:] is Relation-like RAT -valued INT -valued finite V59() V60() V61() V62() set

bool [:1,1:] is finite V32() set

[:[:1,1:],1:] is Relation-like RAT -valued INT -valued finite V59() V60() V61() V62() set

bool [:[:1,1:],1:] is finite V32() set

[:[:1,1:],REAL:] is Relation-like V59() V60() V61() set

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

[:[:REAL,REAL:],REAL:] is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set

bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite non empty-membered set

2 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

[:2,2:] is Relation-like RAT -valued INT -valued finite V59() V60() V61() V62() set

[:[:2,2:],REAL:] is Relation-like V59() V60() V61() set

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

TOP-REAL 2 is non empty non trivial TopSpace-like T_2 V156() V181() V182() V183() V184() V185() V186() V187() strict add-continuous Mult-continuous RLTopStruct

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

the carrier of (TOP-REAL 2) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (TOP-REAL 2)

[: the carrier of (TOP-REAL 2),REAL:] is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set

bool [: the carrier of (TOP-REAL 2),REAL:] is non empty non trivial non finite non empty-membered set

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

[:COMPLEX,COMPLEX:] is non empty non trivial Relation-like non finite non empty-membered V59() set

bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite non empty-membered set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial Relation-like non finite non empty-membered V59() set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite non empty-membered set

[:RAT,RAT:] is non empty non trivial Relation-like RAT -valued non finite non empty-membered V59() V60() V61() set

bool [:RAT,RAT:] is non empty non trivial non finite non empty-membered set

[:[:RAT,RAT:],RAT:] is non empty non trivial Relation-like RAT -valued non finite non empty-membered V59() V60() V61() set

bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite non empty-membered set

[:INT,INT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite non empty-membered V59() V60() V61() set

bool [:INT,INT:] is non empty non trivial non finite non empty-membered set

[:[:INT,INT:],INT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite non empty-membered V59() V60() V61() set

bool [:[:INT,INT:],INT:] is non empty non trivial non finite non empty-membered set

[:NAT,NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite non empty-membered V59() V60() V61() V62() set

[:[:NAT,NAT:],NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite non empty-membered V59() V60() V61() V62() set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite non empty-membered set

[:COMPLEX,REAL:] is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set

bool [:COMPLEX,REAL:] is non empty non trivial non finite non empty-membered set

K567() is Relation-like NAT -defined Function-like total set

3 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

4 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

0 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

proj1 is Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like V43( the carrier of (TOP-REAL 2), REAL ) V59() V60() V61() Element of bool [: the carrier of (TOP-REAL 2),REAL:]

proj2 is Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like V43( the carrier of (TOP-REAL 2), REAL ) V59() V60() V61() Element of bool [: the carrier of (TOP-REAL 2),REAL:]

dom {} is set

rng {} is set

C is non empty non empty-membered set

C * is non empty functional FinSequence-membered FinSequenceSet of C

n is non empty set

<*n*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support set

<*<*n*>*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Function-yielding V81() FinSequence-yielding finite-support set

rng <*<*n*>*> is non empty trivial finite 1 -element set

{<*n*>} is non empty trivial functional finite V32() 1 -element with_non-empty_elements non empty-membered set

G is Relation-like NAT -defined C * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() FinSequence-yielding finite-support FinSequence of C *

rng G is functional finite FinSequence-membered Element of bool (C *)

bool (C *) is set

C is Relation-like non-empty Function-like Function-yielding V81() set

rngs C is Relation-like Function-like set

n is set

dom (rngs C) is set

dom C is set

(rngs C) . n is set

C . n is Relation-like Function-like set

rng (C . n) is set

C is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

n is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

LSeg (C,n) is non empty functional closed closed boundary connected bounded bounded compact compact convex Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

{C,n} is functional finite V32() set

(LSeg (C,n)) \ {C,n} is functional Element of bool the carrier of (TOP-REAL 2)

Cl ((LSeg (C,n)) \ {C,n}) is functional Element of bool the carrier of (TOP-REAL 2)

Euclid 2 is non empty strict Reflexive discerning symmetric triangle MetrStruct

REAL 2 is non empty functional FinSequence-membered FinSequenceSet of REAL

2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

Pitag_dist 2 is Relation-like [:(REAL 2),(REAL 2):] -defined REAL -valued Function-like V43([:(REAL 2),(REAL 2):], REAL ) V59() V60() V61() Element of bool [:[:(REAL 2),(REAL 2):],REAL:]

[:(REAL 2),(REAL 2):] is Relation-like set

[:[:(REAL 2),(REAL 2):],REAL:] is Relation-like V59() V60() V61() set

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

MetrStruct(# (REAL 2),(Pitag_dist 2) #) is strict MetrStruct

the carrier of (Euclid 2) is non empty set

i1 is functional Element of bool the carrier of (TOP-REAL 2)

the topology of (TOP-REAL 2) is Element of bool (bool the carrier of (TOP-REAL 2))

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

TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is strict TopStruct

TopSpaceMetr (Euclid 2) is TopStruct

the carrier of (TopSpaceMetr (Euclid 2)) is set

bool the carrier of (TopSpaceMetr (Euclid 2)) is set

j2 is Element of bool the carrier of (TopSpaceMetr (Euclid 2))

G is Element of the carrier of (Euclid 2)

j2 is V11() real ext-real set

Ball (G,j2) is Element of bool the carrier of (Euclid 2)

bool the carrier of (Euclid 2) is set

j4 is V11() real ext-real Element of REAL

j4 / 2 is V11() real ext-real Element of REAL

f is Element of the carrier of (Euclid 2)

dist (G,f) is V11() real ext-real Element of REAL

(dist (G,f)) / 2 is V11() real ext-real Element of REAL

min ((j4 / 2),((dist (G,f)) / 2)) is V11() real ext-real set

(min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)) is V11() real ext-real Element of REAL

1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) is V11() real ext-real Element of REAL

(1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

(1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

i0 is Element of the carrier of (Euclid 2)

j0 is Relation-like NAT -defined REAL -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of REAL 2

n is Relation-like NAT -defined REAL -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of REAL 2

j is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

i1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

j - i1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

K268(i1) is Relation-like Function-like V59() set

K38(1) is V11() real integer ext-real non positive set

K38(1) * i1 is Relation-like Function-like set

K239(j,K268(i1)) is Relation-like Function-like set

dist (G,i0) is V11() real ext-real Element of REAL

i is Relation-like NAT -defined REAL -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of REAL 2

j0 - i is Relation-like NAT -defined REAL -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of REAL 2

K268(i) is Relation-like Function-like V59() set

K38(1) * i is Relation-like Function-like set

K239(j0,K268(i)) is Relation-like Function-like set

|.(j0 - i).| is V11() real ext-real non negative Element of REAL

(1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

j - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

K268(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)) is Relation-like Function-like V59() set

K38(1) * ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j) is Relation-like Function-like set

K239(j,K268(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j))) is Relation-like Function-like set

((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

(j - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1)) is Relation-like Function-like V59() set

K38(1) * (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1) is Relation-like Function-like set

K239((j - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)),K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1))) is Relation-like Function-like set

|.((j - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1)).| is V11() real ext-real non negative Element of REAL

1 * j is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

(1 * j) - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

K239((1 * j),K268(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j))) is Relation-like Function-like set

((1 * j) - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

K239(((1 * j) - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)),K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1))) is Relation-like Function-like set

|.(((1 * j) - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1)).| is V11() real ext-real non negative Element of REAL

- 1 is V11() real integer ext-real non positive Element of REAL

(- 1) * (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) is V11() real ext-real Element of REAL

((- 1) * (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))))) * j is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

(1 * j) + (((- 1) * (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))))) * j) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

((1 * j) + (((- 1) * (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))))) * j)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

K239(((1 * j) + (((- 1) * (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))))) * j)),K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1))) is Relation-like Function-like set

|.(((1 * j) + (((- 1) * (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))))) * j)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1)).| is V11() real ext-real non negative Element of REAL

- (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) is V11() real ext-real Element of REAL

1 + (- (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))))) is V11() real ext-real Element of REAL

(1 + (- (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))))) * j is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

((1 + (- (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))))) * j) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

K239(((1 + (- (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))))) * j),K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1))) is Relation-like Function-like set

|.(((1 + (- (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))))) * j) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1)).| is V11() real ext-real non negative Element of REAL

((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * j is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

(- 1) * ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) is V11() real ext-real Element of REAL

((- 1) * ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * i1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

(((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * j) + (((- 1) * ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

|.((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * j) + (((- 1) * ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * i1)).| is V11() real ext-real non negative Element of REAL

(- 1) * i1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * ((- 1) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

(((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * j) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * ((- 1) * i1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

|.((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * j) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * ((- 1) * i1))).| is V11() real ext-real non negative Element of REAL

j + ((- 1) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (j + ((- 1) * i1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

|.(((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (j + ((- 1) * i1))).| is V11() real ext-real non negative Element of REAL

- i1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

j + (- i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (j + (- i1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

|.(((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (j + (- i1))).| is V11() real ext-real non negative Element of REAL

((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (j - i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL

|.(((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (j - i1)).| is V11() real ext-real non negative Element of REAL

abs ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) is V11() real ext-real Element of REAL

j1 is Relation-like NAT -defined REAL -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of REAL 2

|.j1.| is V11() real ext-real non negative Element of REAL

(abs ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * |.j1.| is V11() real ext-real Element of REAL

|.(j - i1).| is V11() real ext-real non negative Element of REAL

((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * |.(j - i1).| is V11() real ext-real Element of REAL

((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (dist (G,f)) is V11() real ext-real Element of REAL

j4 / 1 is V11() real ext-real Element of REAL

Ball (G,j4) is Element of bool the carrier of (Euclid 2)

((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * C is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * C is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * C) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

(1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) + ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) is V11() real ext-real Element of REAL

((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) + ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) + ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

(dist (G,f)) / 1 is V11() real ext-real Element of REAL

(1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * n is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

(1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * n) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * n) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) + ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * n is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) + ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)) is Relation-like Function-like V59() set

K38(1) * (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like Function-like set

K239((((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)),K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n))) is Relation-like Function-like set

(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)) - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)) - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

K268(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C)) is Relation-like Function-like V59() set

K38(1) * ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) is Relation-like Function-like set

K239((((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)),K268(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C))) is Relation-like Function-like set

C is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

n is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

LSeg (C,n) is non empty functional closed closed boundary connected bounded bounded compact compact convex Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

{C,n} is functional finite V32() set

(LSeg (C,n)) \ {C,n} is functional Element of bool the carrier of (TOP-REAL 2)

Cl ((LSeg (C,n)) \ {C,n}) is functional Element of bool the carrier of (TOP-REAL 2)

Cl (LSeg (C,n)) is functional connected bounded convex Element of bool the carrier of (TOP-REAL 2)

G is set

((LSeg (C,n)) \ {C,n}) \/ {C,n} is set

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

Cl C is functional Element of bool the carrier of (TOP-REAL 2)

n is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

G is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

LSeg (n,G) is non empty functional closed closed boundary connected bounded bounded compact compact convex Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

{n,G} is functional finite V32() set

(LSeg (n,G)) \ {n,G} is functional Element of bool the carrier of (TOP-REAL 2)

Cl ((LSeg (n,G)) \ {n,G}) is functional Element of bool the carrier of (TOP-REAL 2)

{ [b

n is set

G is V11() real ext-real Element of REAL

f is V11() real ext-real Element of REAL

[G,f] is set

{G,f} is finite V69() V70() V71() set

{G} is non empty trivial finite 1 -element V69() V70() V71() set

{{G,f},{G}} is finite V32() set

() is Relation-like REAL -defined REAL -valued V59() V60() V61() Element of bool [:REAL,REAL:]

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

n is V11() real ext-real Element of REAL

[C,n] is set

{C,n} is finite V69() V70() V71() set

{C} is non empty trivial finite 1 -element V69() V70() V71() set

{{C,n},{C}} is finite V32() set

G is V11() real ext-real Element of REAL

f is V11() real ext-real Element of REAL

[G,f] is set

{G,f} is finite V69() V70() V71() set

{G} is non empty trivial finite 1 -element V69() V70() V71() set

{{G,f},{G}} is finite V32() set

C is set

[C,C] is set

{C,C} is finite set

{C} is non empty trivial finite 1 -element set

{{C,C},{C}} is finite V32() set

n is V11() real ext-real Element of REAL

C is set

n is set

[C,n] is set

{C,n} is finite set

{C} is non empty trivial finite 1 -element set

{{C,n},{C}} is finite V32() set

[n,C] is set

{n,C} is finite set

{n} is non empty trivial finite 1 -element set

{{n,C},{n}} is finite V32() set

G is V11() real ext-real Element of REAL

f is V11() real ext-real Element of REAL

C is set

n is set

G is set

[C,n] is set

{C,n} is finite set

{C} is non empty trivial finite 1 -element set

{{C,n},{C}} is finite V32() set

[n,G] is set

{n,G} is finite set

{n} is non empty trivial finite 1 -element set

{{n,G},{n}} is finite V32() set

[C,G] is set

{C,G} is finite set

{{C,G},{C}} is finite V32() set

f is V11() real ext-real Element of REAL

i1 is V11() real ext-real Element of REAL

j2 is V11() real ext-real Element of REAL

C is set

n is set

[C,n] is set

{C,n} is finite set

{C} is non empty trivial finite 1 -element set

{{C,n},{C}} is finite V32() set

[n,C] is set

{n,C} is finite set

{n} is non empty trivial finite 1 -element set

{{n,C},{n}} is finite V32() set

G is V11() real ext-real Element of REAL

f is V11() real ext-real Element of REAL

field () is set

dom () is set

rng () is V69() V70() V71() set

(dom ()) \/ (rng ()) is set

REAL \/ REAL is V69() V70() V71() set

dom () is V69() V70() V71() Element of bool REAL

C is set

n is V11() real ext-real Element of REAL

[n,n] is set

{n,n} is finite V69() V70() V71() set

{n} is non empty trivial finite 1 -element V69() V70() V71() set

{{n,n},{n}} is finite V32() set

C is finite V69() V70() V71() Element of bool REAL

SgmX ((),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

dom (SgmX ((),C)) is finite set

f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

(SgmX ((),C)) . f is V11() real ext-real Element of REAL

(SgmX ((),C)) . G is V11() real ext-real Element of REAL

dom (SgmX ((),C)) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

(SgmX ((),C)) /. G is V11() real ext-real Element of REAL

(SgmX ((),C)) /. f is V11() real ext-real Element of REAL

[((SgmX ((),C)) . G),((SgmX ((),C)) . f)] is set

{((SgmX ((),C)) . G),((SgmX ((),C)) . f)} is finite V69() V70() V71() set

{((SgmX ((),C)) . G)} is non empty trivial finite 1 -element V69() V70() V71() set

{{((SgmX ((),C)) . G),((SgmX ((),C)) . f)},{((SgmX ((),C)) . G)}} is finite V32() set

C is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

rng C is finite V69() V70() V71() Element of bool REAL

Incr C is Relation-like NAT -defined REAL -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V59() V60() V61() increasing V65() finite-support FinSequence of REAL

n is finite V69() V70() V71() Element of bool REAL

SgmX ((),n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

rng (SgmX ((),n)) is finite V69() V70() V71() Element of bool REAL

G is Relation-like NAT -defined REAL -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V59() V60() V61() increasing V65() finite-support FinSequence of REAL

len G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

card (rng C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega

C is finite V69() V70() V71() Element of bool REAL

SgmX ((),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

C is non empty set

bool C is set

[:C,C:] is Relation-like set

bool [:C,C:] is set

n is finite Element of bool C

card n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega

G is Relation-like C -defined C -valued total reflexive antisymmetric transitive being_linear-order Element of bool [:C,C:]

SgmX (G,n) is Relation-like NAT -defined C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of C

len (SgmX (G,n)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

field G is set

dom G is set

rng G is set

(dom G) \/ (rng G) is set

C is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)

X_axis C is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

proj1 * C is Relation-like NAT -defined REAL -valued Function-like finite V59() V60() V61() finite-support Element of bool [:NAT,REAL:]

[:NAT,REAL:] is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set

bool [:NAT,REAL:] is non empty non trivial non finite non empty-membered set

len (X_axis C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

dom (X_axis C) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

dom C is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

G is ordinal natural V11() real integer finite cardinal ext-real non negative set

(X_axis C) . G is V11() real ext-real Element of REAL

n . G is V11() real ext-real Element of REAL

C /. G is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

C . G is Relation-like Function-like set

(C /. G) `1 is V11() real ext-real Element of REAL

(C /. G) . 1 is V11() real ext-real Element of REAL

proj1 . (C . G) is V11() real ext-real Element of REAL

len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

C is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)

Y_axis C is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

proj2 * C is Relation-like NAT -defined REAL -valued Function-like finite V59() V60() V61() finite-support Element of bool [:NAT,REAL:]

[:NAT,REAL:] is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set

bool [:NAT,REAL:] is non empty non trivial non finite non empty-membered set

len (Y_axis C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

dom (Y_axis C) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

dom C is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

G is ordinal natural V11() real integer finite cardinal ext-real non negative set

(Y_axis C) . G is V11() real ext-real Element of REAL

n . G is V11() real ext-real Element of REAL

C /. G is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

C . G is Relation-like Function-like set

(C /. G) `2 is V11() real ext-real Element of REAL

(C /. G) . 2 is V11() real ext-real Element of REAL

proj2 . (C . G) is V11() real ext-real Element of REAL

len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

C is non empty set

C * is non empty functional FinSequence-membered FinSequenceSet of C

n is Relation-like NAT -defined C * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() FinSequence-yielding finite-support FinSequence of C *

Values n is finite set

bool C is set

rng n is functional finite FinSequence-membered Element of bool (C *)

bool (C *) is set

{ (rng b

f is set

i1 is Relation-like NAT -defined C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of C *

rng i1 is finite Element of bool C

union { (rng b

C is non empty with_non-empty_elements non empty-membered set

C * is non empty functional FinSequence-membered FinSequenceSet of C

n is non empty Relation-like non-empty NAT -defined C * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() FinSequence-yielding finite-support FinSequence of C *

(C,n) is finite Element of bool C

bool C is set

rngs n is Relation-like non-empty Function-like set

dom (rngs n) is set

dom n is non empty finite V69() V70() V71() V72() V73() V74() Element of bool NAT

rng (rngs n) is with_non-empty_elements set

Union (rngs n) is set

G is non empty with_non-empty_elements non empty-membered set

union G is non empty set

C is non empty set

C * is non empty functional FinSequence-membered FinSequenceSet of C

n is Relation-like NAT -defined C * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular FinSequence-yielding finite-support FinSequence of C *

width n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

Seg (width n) is finite width n -element V69() V70() V71() V72() V73() V74() Element of bool NAT

(C,n) is finite Element of bool C

bool C is set

G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

Col (n,G) is Relation-like NAT -defined C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (len n) -tuples_on C

len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

(len n) -tuples_on C is functional FinSequence-membered FinSequenceSet of C

rng (Col (n,G)) is finite Element of bool C

f is set

dom (Col (n,G)) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

i1 is set

(Col (n,G)) . i1 is set

j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

len (Col (n,G)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

[j2,G] is set

{j2,G} is finite V32() V69() V70() V71() V72() V73() V74() set

{j2} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set

{{j2,G},{j2}} is finite V32() set

Indices n is set

{ (n * (b

dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

(Col (n,G)) . j2 is set

n * (j2,G) is Element of C

C is non empty set

C * is non empty functional FinSequence-membered FinSequenceSet of C

n is Relation-like NAT -defined C * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular FinSequence-yielding finite-support FinSequence of C *

dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

(C,n) is finite Element of bool C

bool C is set

G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

Line (n,G) is Relation-like NAT -defined C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width n) -tuples_on C

width n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

(width n) -tuples_on C is functional FinSequence-membered FinSequenceSet of C

rng (Line (n,G)) is finite Element of bool C

len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

f is set

dom (Line (n,G)) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

i1 is set

(Line (n,G)) . i1 is set

j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

len (Line (n,G)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

[G,j2] is set

{G,j2} is finite V32() V69() V70() V71() V72() V73() V74() set

{G} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set

{{G,j2},{G}} is finite V32() set

Indices n is set

{ (n * (b

Seg (width n) is finite width n -element V69() V70() V71() V72() V73() V74() Element of bool NAT

(Line (n,G)) . j2 is set

n * (G,j2) is Element of C

C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *

len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

( the carrier of (TOP-REAL 2),C) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)

proj1 .: ( the carrier of (TOP-REAL 2),C) is finite V69() V70() V71() Element of bool REAL

card (proj1 .: ( the carrier of (TOP-REAL 2),C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega

width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

Seg (width C) is finite width C -element V69() V70() V71() V72() V73() V74() Element of bool NAT

Col (C,1) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support Element of (len C) -tuples_on the carrier of (TOP-REAL 2)

(len C) -tuples_on the carrier of (TOP-REAL 2) is functional FinSequence-membered FinSequenceSet of the carrier of (TOP-REAL 2)

X_axis (Col (C,1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

n is Relation-like NAT -defined REAL -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V59() V60() V61() increasing V65() finite-support FinSequence of REAL

rng n is finite V69() V70() V71() Element of bool REAL

card (rng n) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega

len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

len (Col (C,1)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

proj1 * (Col (C,1)) is Relation-like NAT -defined REAL -valued Function-like finite V59() V60() V61() finite-support Element of bool [:NAT,REAL:]

[:NAT,REAL:] is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set

bool [:NAT,REAL:] is non empty non trivial non finite non empty-membered set

rng (proj1 * (Col (C,1))) is finite V69() V70() V71() Element of bool REAL

rng (Col (C,1)) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)

proj1 .: (rng (Col (C,1))) is finite V69() V70() V71() Element of bool REAL

C is Relation-like NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *

( the carrier of (TOP-REAL 2),C) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)

proj1 .: ( the carrier of (TOP-REAL 2),C) is finite V69() V70() V71() Element of bool REAL

card (proj1 .: ( the carrier of (TOP-REAL 2),C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega

len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set

len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

dom C is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

rng n is finite set

G is set

Indices C is set

{ (C * (b

f is set

proj1 . f is V11() real ext-real Element of REAL

i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

C * (i1,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

[i1,j2] is set

{i1,j2} is finite V32() V69() V70() V71() V72() V73() V74() set

{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set

{{i1,j2},{i1}} is finite V32() set

width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

j2 is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

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

j2 . 1 is V11() real ext-real Element of REAL

C * (i1,1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

(C * (i1,1)) `1 is V11() real ext-real Element of REAL

(C * (i1,1)) . 1 is V11() real ext-real Element of REAL

proj1 . (C * (i1,1)) is V11() real ext-real Element of REAL

n . i1 is set

card (dom C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega

C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *

len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

( the carrier of (TOP-REAL 2),C) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)

proj1 .: ( the carrier of (TOP-REAL 2),C) is finite V69() V70() V71() Element of bool REAL

card (proj1 .: ( the carrier of (TOP-REAL 2),C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega

C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular Y_increasing-in-line FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *

width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

( the carrier of (TOP-REAL 2),C) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)

proj2 .: ( the carrier of (TOP-REAL 2),C) is finite V69() V70() V71() Element of bool REAL

card (proj2 .: ( the carrier of (TOP-REAL 2),C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega

len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

dom C is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

Line (C,1) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support Element of (width C) -tuples_on the carrier of (TOP-REAL 2)

(width C) -tuples_on the carrier of (TOP-REAL 2) is functional FinSequence-membered FinSequenceSet of the carrier of (TOP-REAL 2)

Y_axis (Line (C,1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL

n is Relation-like NAT -defined REAL -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V59() V60() V61() increasing V65() finite-support FinSequence of REAL

rng n is finite V69() V70() V71() Element of bool REAL

card (rng n) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega

len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

len (Line (C,1)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

proj2 * (Line (C,1)) is Relation-like NAT -defined REAL -valued Function-like finite V59() V60() V61() finite-support Element of bool [:NAT,REAL:]

[:NAT,REAL:] is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set

bool [:NAT,REAL:] is non empty non trivial non finite non empty-membered set

rng (proj2 * (Line (C,1))) is finite V69() V70() V71() Element of bool REAL

rng (Line (C,1)) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)

proj2 .: (rng (Line (C,1))) is finite V69() V70() V71() Element of bool REAL

C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular Y_equal-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *

( the carrier of (TOP-REAL 2),C) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)

proj2 .: ( the carrier of (TOP-REAL 2),C) is finite V69() V70() V71() Element of bool REAL

card (proj2 .: ( the carrier of (TOP-REAL 2),C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega

width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set

len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

Seg (width C) is finite width C -element V69() V70() V71() V72() V73() V74() Element of bool NAT

rng n is finite set

G is set

Indices C is set

{ (C * (b

f is set

proj2 . f is V11() real ext-real Element of REAL

i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

C * (i1,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

[i1,j2] is set

{i1,j2} is finite V32() V69() V70() V71() V72() V73() V74() set

{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set

{{i1,j2},{i1}} is finite V32() set

len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

j2 is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

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

j2 . 2 is V11() real ext-real Element of REAL

C * (1,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

(C * (1,j2)) `2 is V11() real ext-real Element of REAL

(C * (1,j2)) . 2 is V11() real ext-real Element of REAL

proj2 . (C * (1,j2)) is V11() real ext-real Element of REAL

n . j2 is set

card (Seg (width C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega

C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular Y_equal-in-column Y_increasing-in-line FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *

width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

( the carrier of (TOP-REAL 2),C) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)

proj2 .: ( the carrier of (TOP-REAL 2),C) is finite V69() V70() V71() Element of bool REAL

card (proj2 .: ( the carrier of (TOP-REAL 2),C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega

C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *

n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)

len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

G + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

LSeg (n,G) is functional Element of bool the carrier of (TOP-REAL 2)

left_cell (n,G,C) is functional Element of bool the carrier of (TOP-REAL 2)

dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

Indices C is set

n /. G is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)

f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

[f,i1] is set

{f,i1} is finite V32() V69() V70() V71() V72() V73() V74() set

{f} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set

{{f,i1},{f}