:: TAXONOM1 semantic presentation

REAL is non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval set

NAT is V106() V107() V108() V109() V110() V111() V112() bounded_below Element of bool REAL

bool REAL is non empty set

omega is V106() V107() V108() V109() V110() V111() V112() bounded_below set

bool omega is non empty set

bool NAT is non empty set

1 is non empty natural V11() ext-real positive non negative real V106() V107() V108() V109() V110() V111() left_end bounded_below Element of NAT

[:1,1:] is non empty set

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

[:[:1,1:],1:] is non empty set

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

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

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

[:REAL,REAL:] is non empty set

[:[:REAL,REAL:],REAL:] is non empty set

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

2 is non empty natural V11() ext-real positive non negative real V106() V107() V108() V109() V110() V111() left_end bounded_below Element of NAT

[:2,2:] is non empty set

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

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

{} is empty finite V48() V106() V107() V108() V109() V110() V111() V112() bounded_below bounded_above real-bounded interval set

0 is empty natural V11() ext-real non positive non negative finite V48() real V106() V107() V108() V109() V110() V111() V112() bounded_below bounded_above real-bounded interval Element of NAT

a is Relation-like Function-like FinSequence-like set

dom a is V106() V107() V108() V109() V110() V111() bounded_below Element of bool NAT

M is natural V11() ext-real real set

M + 1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT

len a is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT

a is Relation-like Function-like FinSequence-like set

dom a is V106() V107() V108() V109() V110() V111() bounded_below Element of bool NAT

M is natural V11() ext-real real set

R is natural V11() ext-real real set

a . M is set

a . R is set

x is natural V11() ext-real real set

a . x is set

x + 1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT

a . (x + 1) is set

y is natural V11() ext-real real set

a . y is set

a . 1 is set

x1 is natural V11() ext-real real set

a . x1 is set

x1 + 1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT

a . (x1 + 1) is set

a . 0 is set

a . 0 is set

x is natural V11() ext-real real set

a . x is set

a is set

[:a,a:] is set

bool [:a,a:] is non empty set

M is Relation-like a -defined a -valued Element of bool [:a,a:]

dom M is Element of bool a

bool a is non empty set

R is set

[R,R] is set

{R,R} is non empty finite set

{R} is non empty finite set

{{R,R},{R}} is non empty finite V48() set

a is set

[:a,a:] is set

bool [:a,a:] is non empty set

M is Relation-like a -defined a -valued Element of bool [:a,a:]

rng M is Element of bool a

bool a is non empty set

R is set

x is set

[x,R] is set

{x,R} is non empty finite set

{x} is non empty finite set

{{x,R},{x}} is non empty finite V48() set

a is set

[:a,a:] is set

bool [:a,a:] is non empty set

M is Relation-like a -defined a -valued Element of bool [:a,a:]

M [*] is Relation-like set

R is set

[R,R] is set

{R,R} is non empty finite set

{R} is non empty finite set

{{R,R},{R}} is non empty finite V48() set

a is set

[:a,a:] is set

bool [:a,a:] is non empty set

M is set

R is set

[M,R] is set

{M,R} is non empty finite set

{M} is non empty finite set

{{M,R},{M}} is non empty finite V48() set

x is Relation-like a -defined a -valued Element of bool [:a,a:]

x [*] is Relation-like set

a is set

[:a,a:] is set

bool [:a,a:] is non empty set

M is Relation-like a -defined a -valued Element of bool [:a,a:]

M [*] is Relation-like set

R is set

x is set

[R,x] is set

{R,x} is non empty finite set

{R} is non empty finite set

{{R,x},{R}} is non empty finite V48() set

field M is set

y is Relation-like Function-like FinSequence-like set

len y is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT

y . 1 is set

y . (len y) is set

Rev y is Relation-like Function-like FinSequence-like set

x1 is Relation-like Function-like FinSequence-like set

y1 is natural V11() ext-real real set

len x1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT

(len y) - 0 is V11() ext-real real set

(len y) - y1 is V11() ext-real real set

Seg (len y) is V106() V107() V108() V109() V110() V111() bounded_below Element of bool NAT

dom y is V106() V107() V108() V109() V110() V111() bounded_below Element of bool NAT

x1 . y1 is set

((len y) - y1) + 1 is V11() ext-real real set

y . (((len y) - y1) + 1) is set

y1 + 1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT

d1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT

y . ((len y) - y1) is set

[(y . ((len y) - y1)),(y . (((len y) - y1) + 1))] is set

{(y . ((len y) - y1)),(y . (((len y) - y1) + 1))} is non empty finite set

{(y . ((len y) - y1))} is non empty finite set

{{(y . ((len y) - y1)),(y . (((len y) - y1) + 1))},{(y . ((len y) - y1))}} is non empty finite V48() set

(len y) - (y1 + 1) is V11() ext-real real set

((len y) - (y1 + 1)) + 1 is V11() ext-real real set

y . (((len y) - (y1 + 1)) + 1) is set

[(y . (((len y) - y1) + 1)),(y . (((len y) - (y1 + 1)) + 1))] is set

{(y . (((len y) - y1) + 1)),(y . (((len y) - (y1 + 1)) + 1))} is non empty finite set

{(y . (((len y) - y1) + 1))} is non empty finite set

{{(y . (((len y) - y1) + 1)),(y . (((len y) - (y1 + 1)) + 1))},{(y . (((len y) - y1) + 1))}} is non empty finite V48() set

x1 . (y1 + 1) is set

[(x1 . y1),(x1 . (y1 + 1))] is set

{(x1 . y1),(x1 . (y1 + 1))} is non empty finite set

{(x1 . y1)} is non empty finite set

{{(x1 . y1),(x1 . (y1 + 1))},{(x1 . y1)}} is non empty finite V48() set

x1 . (len x1) is set

x1 . (len y) is set

x1 . 1 is set

[x,R] is set

{x,R} is non empty finite set

{x} is non empty finite set

{{x,R},{x}} is non empty finite V48() set

a is set

[:a,a:] is set

bool [:a,a:] is non empty set

M is Relation-like a -defined a -valued Element of bool [:a,a:]

M [*] is Relation-like set

R is set

x is set

y is set

[R,x] is set

{R,x} is non empty finite set

{R} is non empty finite set

{{R,x},{R}} is non empty finite V48() set

[x,y] is set

{x,y} is non empty finite set

{x} is non empty finite set

{{x,y},{x}} is non empty finite V48() set

[R,y] is set

{R,y} is non empty finite set

{{R,y},{R}} is non empty finite V48() set

a is non empty set

[:a,a:] is non empty set

bool [:a,a:] is non empty set

M is Relation-like a -defined a -valued Element of bool [:a,a:]

M [*] is Relation-like a -defined a -valued Element of bool [:a,a:]

dom (M [*]) is Element of bool a

bool a is non empty set

field (M [*]) is set

a is non empty set

[:a,a:] is non empty set

bool [:a,a:] is non empty set

M is Relation-like a -defined a -valued Element of bool [:a,a:]

R is Relation-like a -defined a -valued Element of bool [:a,a:]

M [*] is Relation-like a -defined a -valued Element of bool [:a,a:]

R [*] is Relation-like a -defined a -valued Element of bool [:a,a:]

field M is set

field R is set

x is set

y is set

x1 is set

[y,x1] is set

{y,x1} is non empty finite set

{y} is non empty finite set

{{y,x1},{y}} is non empty finite V48() set

y1 is Relation-like Function-like FinSequence-like set

len y1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT

y1 . 1 is set

y1 . (len y1) is set

d1 is natural V11() ext-real real set

y1 . d1 is set

d1 + 1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT

y1 . (d1 + 1) is set

[(y1 . d1),(y1 . (d1 + 1))] is set

{(y1 . d1),(y1 . (d1 + 1))} is non empty finite set

{(y1 . d1)} is non empty finite set

{{(y1 . d1),(y1 . (d1 + 1))},{(y1 . d1)}} is non empty finite V48() set

a is non empty set

M is non empty with_non-empty_elements a_partition of a

{a} is non empty finite set

{{a}} is non empty finite V48() set

R is non empty with_non-empty_elements a_partition of a

a is non empty set

%I a is non empty with_non-empty_elements a_partition of a

id a is non empty Relation-like a -defined a -valued total Element of bool [:a,a:]

[:a,a:] is non empty set

bool [:a,a:] is non empty set

Class (id a) is non empty with_non-empty_elements a_partition of a

{a} is non empty finite set

M is set

a is non empty set

PARTITIONS a is set

bool (PARTITIONS a) is non empty set

{a} is non empty finite set

{{a}} is non empty finite V48() set

M is Element of bool (PARTITIONS a)

R is non empty with_non-empty_elements a_partition of a

x is non empty with_non-empty_elements a_partition of a

a is non empty set

{a} is non empty finite set

{{a}} is non empty finite V48() set

PARTITIONS a is set

bool (PARTITIONS a) is non empty set

M is Element of bool (PARTITIONS a)

R is non empty with_non-empty_elements a_partition of a

x is non empty with_non-empty_elements a_partition of a

a is non empty set

%I a is non empty with_non-empty_elements a_partition of a

id a is non empty Relation-like a -defined a -valued total Element of bool [:a,a:]

[:a,a:] is non empty set

bool [:a,a:] is non empty set

Class (id a) is non empty with_non-empty_elements a_partition of a

{(%I a)} is non empty finite set

PARTITIONS a is set

bool (PARTITIONS a) is non empty set

M is Element of bool (PARTITIONS a)

R is non empty with_non-empty_elements a_partition of a

x is non empty with_non-empty_elements a_partition of a

a is non empty set

PARTITIONS a is set

bool (PARTITIONS a) is non empty set

{a} is non empty finite set

%I a is non empty with_non-empty_elements a_partition of a

id a is non empty Relation-like a -defined a -valued total Element of bool [:a,a:]

[:a,a:] is non empty set

bool [:a,a:] is non empty set

Class (id a) is non empty with_non-empty_elements a_partition of a

{{a},(%I a)} is non empty finite set

M is Element of bool (PARTITIONS a)

R is non empty with_non-empty_elements a_partition of a

x is non empty with_non-empty_elements a_partition of a

a is non empty set

PARTITIONS a is set

bool (PARTITIONS a) is non empty set

{a} is non empty finite set

%I a is non empty with_non-empty_elements a_partition of a

id a is non empty Relation-like a -defined a -valued total Element of bool [:a,a:]

[:a,a:] is non empty set

bool [:a,a:] is non empty set

Class (id a) is non empty with_non-empty_elements a_partition of a

{{a},(%I a)} is non empty finite set

M is Element of bool (PARTITIONS a)

a is non empty set

PARTITIONS a is set

bool (PARTITIONS a) is non empty set

{a} is non empty finite set

%I a is non empty with_non-empty_elements a_partition of a

id a is non empty Relation-like a -defined a -valued total Element of bool [:a,a:]

[:a,a:] is non empty set

bool [:a,a:] is non empty set

Class (id a) is non empty with_non-empty_elements a_partition of a

{{a},(%I a)} is non empty finite set

M is Element of bool (PARTITIONS a)

a is non empty set

[:a,a:] is non empty set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

bool [:a,a:] is non empty set

M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]

R is V11() ext-real real set

x is Relation-like a -defined a -valued Element of bool [:a,a:]

y is Element of a

x1 is Element of a

[y,x1] is set

{y,x1} is non empty finite set

{y} is non empty finite set

{{y,x1},{y}} is non empty finite V48() set

M . (y,x1) is V11() ext-real real Element of REAL

M . [y,x1] is set

y1 is Element of a

d1 is Element of a

M . (y1,d1) is V11() ext-real real Element of REAL

[y1,d1] is set

{y1,d1} is non empty finite set

{y1} is non empty finite set

{{y1,d1},{y1}} is non empty finite V48() set

M . [y1,d1] is set

x is Relation-like a -defined a -valued Element of bool [:a,a:]

y is Relation-like a -defined a -valued Element of bool [:a,a:]

x1 is set

y1 is set

[x1,y1] is set

{x1,y1} is non empty finite set

{x1} is non empty finite set

{{x1,y1},{x1}} is non empty finite V48() set

d1 is Element of a

y is Element of a

M . (d1,y) is V11() ext-real real Element of REAL

[d1,y] is set

{d1,y} is non empty finite set

{d1} is non empty finite set

{{d1,y},{d1}} is non empty finite V48() set

M . [d1,y] is set

x1 is set

y1 is set

[x1,y1] is set

{x1,y1} is non empty finite set

{x1} is non empty finite set

{{x1,y1},{x1}} is non empty finite V48() set

d1 is Element of a

y is Element of a

M . (d1,y) is V11() ext-real real Element of REAL

[d1,y] is set

{d1,y} is non empty finite set

{d1} is non empty finite set

{{d1,y},{d1}} is non empty finite V48() set

M . [d1,y] is set

a is non empty set

[:a,a:] is non empty set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]

R is V11() ext-real real set

(a,M,R) is Relation-like a -defined a -valued Element of bool [:a,a:]

bool [:a,a:] is non empty set

x is set

y is Element of a

M . (y,y) is V11() ext-real real Element of REAL

[y,y] is set

{y,y} is non empty finite set

{y} is non empty finite set

{{y,y},{y}} is non empty finite V48() set

M . [y,y] is set

[x,x] is set

{x,x} is non empty finite set

{x} is non empty finite set

{{x,x},{x}} is non empty finite V48() set

a is non empty set

[:a,a:] is non empty set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]

R is V11() ext-real real set

(a,M,R) is Relation-like a -defined a -valued Element of bool [:a,a:]

bool [:a,a:] is non empty set

x is set

y is set

[x,y] is set

{x,y} is non empty finite set

{x} is non empty finite set

{{x,y},{x}} is non empty finite V48() set

x1 is Element of a

y1 is Element of a

M . (x1,y1) is V11() ext-real real Element of REAL

[x1,y1] is set

{x1,y1} is non empty finite set

{x1} is non empty finite set

{{x1,y1},{x1}} is non empty finite V48() set

M . [x1,y1] is set

M . (y1,x1) is V11() ext-real real Element of REAL

[y1,x1] is set

{y1,x1} is non empty finite set

{y1} is non empty finite set

{{y1,x1},{y1}} is non empty finite V48() set

M . [y1,x1] is set

[y,x] is set

{y,x} is non empty finite set

{y} is non empty finite set

{{y,x},{y}} is non empty finite V48() set

a is non empty set

[:a,a:] is non empty set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

bool [:a,a:] is non empty set

M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]

R is V11() ext-real real set

(a,M,R) is Relation-like a -defined a -valued Element of bool [:a,a:]

dom (a,M,R) is Element of bool a

bool a is non empty set

field (a,M,R) is set

rng (a,M,R) is Element of bool a

a \/ (rng (a,M,R)) is non empty set

a is non empty set

[:a,a:] is non empty set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]

R is V11() ext-real real set

x is V11() ext-real real set

(a,M,R) is Relation-like a -defined a -valued Element of bool [:a,a:]

bool [:a,a:] is non empty set

(a,M,x) is Relation-like a -defined a -valued Element of bool [:a,a:]

y is set

x1 is set

y1 is set

[x1,y1] is set

{x1,y1} is non empty finite set

{x1} is non empty finite set

{{x1,y1},{x1}} is non empty finite V48() set

d1 is Element of a

y is Element of a

M . (d1,y) is V11() ext-real real Element of REAL

[d1,y] is set

{d1,y} is non empty finite set

{d1} is non empty finite set

{{d1,y},{d1}} is non empty finite V48() set

M . [d1,y] is set

a is set

[:a,a:] is set

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

bool [:[:a,a:],REAL:] is non empty set

a is non empty set

[:a,a:] is non empty set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]

(a,M,0) is Relation-like a -defined a -valued Element of bool [:a,a:]

bool [:a,a:] is non empty set

R is set

x is set

[R,x] is set

{R,x} is non empty finite set

{R} is non empty finite set

{{R,x},{R}} is non empty finite V48() set

y is Element of a

x1 is Element of a

M . (y,x1) is V11() ext-real real Element of REAL

[y,x1] is set

{y,x1} is non empty finite set

{y} is non empty finite set

{{y,x1},{y}} is non empty finite V48() set

M . [y,x1] is set

a is non empty set

[:a,a:] is non empty set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]

(a,M,0) is Relation-like a -defined a -valued Element of bool [:a,a:]

bool [:a,a:] is non empty set

R is Element of a

[R,R] is set

{R,R} is non empty finite set

{R} is non empty finite set

{{R,R},{R}} is non empty finite V48() set

M . (R,R) is V11() ext-real real Element of REAL

M . [R,R] is set

a is non empty set

[:a,a:] is non empty set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

bool [:a,a:] is non empty set

M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]

R is V11() ext-real real set

(a,M,R) is Relation-like a -defined a -valued Element of bool [:a,a:]

(a,M,R) [*] is Relation-like a -defined a -valued Element of bool [:a,a:]

x is set

y is set

[x,y] is set

{x,y} is non empty finite set

{x} is non empty finite set

{{x,y},{x}} is non empty finite V48() set

x1 is Element of a

y1 is Element of a

M . (x1,y1) is V11() ext-real real Element of REAL

[x1,y1] is set

{x1,y1} is non empty finite set

{x1} is non empty finite set

{{x1,y1},{x1}} is non empty finite V48() set

M . [x1,y1] is set

M . (y1,x1) is V11() ext-real real Element of REAL

[y1,x1] is set

{y1,x1} is non empty finite set

{y1} is non empty finite set

{{y1,x1},{y1}} is non empty finite V48() set

M . [y1,x1] is set

[y,x] is set

{y,x} is non empty finite set

{y} is non empty finite set

{{y,x},{y}} is non empty finite V48() set

a is set

M is non empty set

[:M,M:] is non empty set

[:[:M,M:],REAL:] is non empty set

bool [:[:M,M:],REAL:] is non empty set

bool [:M,M:] is non empty set

R is V11() ext-real non negative real set

x is V11() ext-real non negative real set

y is Relation-like [:M,M:] -defined REAL -valued Function-like Element of bool [:[:M,M:],REAL:]

(M,y,R) is Relation-like M -defined M -valued Element of bool [:M,M:]

(M,y,R) [*] is Relation-like M -defined M -valued Element of bool [:M,M:]

(M,y,x) is Relation-like M -defined M -valued Element of bool [:M,M:]

(M,y,x) [*] is Relation-like M -defined M -valued Element of bool [:M,M:]

x1 is Relation-like M -defined M -valued total symmetric transitive Element of bool [:M,M:]

y1 is Relation-like M -defined M -valued total symmetric transitive Element of bool [:M,M:]

Class (x1,a) is Element of bool M

bool M is non empty set

Class (y1,a) is Element of bool M

d1 is set

[d1,a] is set

{d1,a} is non empty finite set

{d1} is non empty finite set

{{d1,a},{d1}} is non empty finite V48() set

a is non empty set

[:a,a:] is non empty set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]

(a,M,0) is Relation-like a -defined a -valued Element of bool [:a,a:]

bool [:a,a:] is non empty set

(a,M,0) [*] is Relation-like a -defined a -valued Element of bool [:a,a:]

R is set

x is set

y is set

[x,y] is set

{x,y} is non empty finite set

{x} is non empty finite set

{{x,y},{x}} is non empty finite V48() set

x1 is Relation-like Function-like FinSequence-like RedSequence of (a,M,0)

x1 . 1 is set

len x1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT

x1 . (len x1) is set

y1 is natural V11() ext-real real set

dom x1 is V106() V107() V108() V109() V110() V111() bounded_below Element of bool NAT

y1 + 1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT

x1 . y1 is set

x1 . (y1 + 1) is set

[(x1 . y1),(x1 . (y1 + 1))] is set

{(x1 . y1),(x1 . (y1 + 1))} is non empty finite set

{(x1 . y1)} is non empty finite set

{{(x1 . y1),(x1 . (y1 + 1))},{(x1 . y1)}} is non empty finite V48() set

0 + 1 is non empty natural V11() ext-real positive non negative real V106() V107() V108() V109() V110() V111() left_end bounded_below Element of NAT

a is non empty set

[:a,a:] is non empty set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

bool [:a,a:] is non empty set

id a is non empty Relation-like set

M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]

(a,M,0) is Relation-like a -defined a -valued Element of bool [:a,a:]

(a,M,0) [*] is Relation-like a -defined a -valued Element of bool [:a,a:]

R is Relation-like a -defined a -valued total symmetric transitive Element of bool [:a,a:]

x is set

y is set

[x,y] is set

{x,y} is non empty finite set

{x} is non empty finite set

{{x,y},{x}} is non empty finite V48() set

x is set

y is set

[x,y] is set

{x,y} is non empty finite set

{x} is non empty finite set

{{x,y},{x}} is non empty finite V48() set

a is non empty set

[:a,a:] is non empty set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

bool [:a,a:] is non empty set

R is Relation-like a -defined a -valued total symmetric transitive Element of bool [:a,a:]

M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]

(a,M,0) is Relation-like a -defined a -valued Element of bool [:a,a:]

(a,M,0) [*] is Relation-like a -defined a -valued Element of bool [:a,a:]

Class R is non empty with_non-empty_elements a_partition of a

%I a is non empty with_non-empty_elements a_partition of a

id a is non empty Relation-like a -defined a -valued total Element of bool [:a,a:]

Class (id a) is non empty with_non-empty_elements a_partition of a

a is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

[:a,a:] is non empty finite set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

M is Relation-like [:a,a:] -defined REAL -valued Function-like V29([:a,a:], REAL ) finite Element of bool [:[:a,a:],REAL:]

rng M is finite V106() V107() V108() bounded_below bounded_above real-bounded Element of bool REAL

R is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

max R is V11() ext-real real set

x is V11() ext-real real set

y is V11() ext-real real Element of a

x1 is V11() ext-real real Element of a

[y,x1] is set

{y,x1} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set

{y} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set

{{y,x1},{y}} is non empty finite V48() set

M . [y,x1] is set

M . (y,x1) is V11() ext-real real Element of REAL

dom M is Relation-like a -defined a -valued finite Element of bool [:a,a:]

bool [:a,a:] is non empty finite V48() set

y1 is V11() ext-real real set

y is V11() ext-real real Element of a

x1 is V11() ext-real real Element of a

M . (y,x1) is V11() ext-real real Element of REAL

[y,x1] is set

{y,x1} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set

{y} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set

{{y,x1},{y}} is non empty finite V48() set

M . [y,x1] is set

a is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

[:a,a:] is non empty finite set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

bool [:a,a:] is non empty finite V48() set

{a} is non empty finite V48() set

M is Relation-like [:a,a:] -defined REAL -valued Function-like V29([:a,a:], REAL ) finite Element of bool [:[:a,a:],REAL:]

rng M is finite V106() V107() V108() bounded_below bounded_above real-bounded Element of bool REAL

R is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

max R is V11() ext-real real set

x is V11() ext-real real set

(a,M,x) is Relation-like a -defined a -valued finite Element of bool [:a,a:]

(a,M,x) [*] is Relation-like a -defined a -valued finite Element of bool [:a,a:]

y is Relation-like a -defined a -valued total symmetric transitive finite Element of bool [:a,a:]

x1 is set

Class (y,x1) is finite V106() V107() V108() bounded_below bounded_above real-bounded Element of bool a

bool a is non empty finite V48() set

d1 is set

y is V11() ext-real real Element of a

y1 is V11() ext-real real Element of a

M . (y,y1) is V11() ext-real real Element of REAL

[y,y1] is set

{y,y1} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set

{y} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set

{{y,y1},{y}} is non empty finite V48() set

M . [y,y1] is set

[d1,x1] is set

{d1,x1} is non empty finite set

{d1} is non empty finite set

{{d1,x1},{d1}} is non empty finite V48() set

x1 is set

y1 is set

Class (y,y1) is finite V106() V107() V108() bounded_below bounded_above real-bounded Element of bool a

bool a is non empty finite V48() set

Class y is non empty with_non-empty_elements finite V48() a_partition of a

x1 is set

y1 is set

Class (y,y1) is finite V106() V107() V108() bounded_below bounded_above real-bounded Element of bool a

y is Relation-like a -defined a -valued total symmetric transitive finite Element of bool [:a,a:]

Class y is non empty with_non-empty_elements finite V48() a_partition of a

a is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

[:a,a:] is non empty finite set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

M is Relation-like [:a,a:] -defined REAL -valued Function-like V29([:a,a:], REAL ) finite Element of bool [:[:a,a:],REAL:]

rng M is finite V106() V107() V108() bounded_below bounded_above real-bounded Element of bool REAL

R is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

max R is V11() ext-real real set

x is V11() ext-real real set

(a,M,x) is Relation-like a -defined a -valued finite Element of bool [:a,a:]

bool [:a,a:] is non empty finite V48() set

(a,M,x) [*] is Relation-like a -defined a -valued finite Element of bool [:a,a:]

y is set

x1 is set

y1 is set

[x1,y1] is set

{x1,y1} is non empty finite set

{x1} is non empty finite set

{{x1,y1},{x1}} is non empty finite V48() set

d1 is V11() ext-real real Element of a

y is V11() ext-real real Element of a

M . (d1,y) is V11() ext-real real Element of REAL

[d1,y] is set

{d1,y} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set

{d1} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set

{{d1,y},{d1}} is non empty finite V48() set

M . [d1,y] is set

a is non empty set

[:a,a:] is non empty set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

PARTITIONS a is set

bool (PARTITIONS a) is non empty set

bool [:a,a:] is non empty set

M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]

R is set

x is set

x is Element of bool (PARTITIONS a)

y is set

y1 is Relation-like a -defined a -valued total symmetric transitive Element of bool [:a,a:]

x1 is V11() ext-real non negative real set

(a,M,x1) is Relation-like a -defined a -valued Element of bool [:a,a:]

(a,M,x1) [*] is Relation-like a -defined a -valued Element of bool [:a,a:]

Class y1 is non empty with_non-empty_elements a_partition of a

R is Element of bool (PARTITIONS a)

x is Element of bool (PARTITIONS a)

a is non empty set

[:a,a:] is non empty set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]

(a,M) is Element of bool (PARTITIONS a)

PARTITIONS a is set

bool (PARTITIONS a) is non empty set

R is V11() ext-real non negative real set

(a,M,R) is Relation-like a -defined a -valued Element of bool [:a,a:]

bool [:a,a:] is non empty set

(a,M,R) [*] is Relation-like a -defined a -valued Element of bool [:a,a:]

x is Relation-like a -defined a -valued total symmetric transitive Element of bool [:a,a:]

Class x is non empty with_non-empty_elements a_partition of a

y is set

a is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

[:a,a:] is non empty finite set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

{a} is non empty finite V48() set

M is Relation-like [:a,a:] -defined REAL -valued Function-like V29([:a,a:], REAL ) finite Element of bool [:[:a,a:],REAL:]

(a,M) is Element of bool (PARTITIONS a)

PARTITIONS a is set

bool (PARTITIONS a) is non empty set

dom M is Relation-like a -defined a -valued finite Element of bool [:a,a:]

bool [:a,a:] is non empty finite V48() set

rng M is finite V106() V107() V108() bounded_below bounded_above real-bounded Element of bool REAL

R is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

max R is V11() ext-real real set

the V11() ext-real real Element of a is V11() ext-real real Element of a

x is V11() ext-real real set

M . ( the V11() ext-real real Element of a, the V11() ext-real real Element of a) is V11() ext-real real Element of REAL

[ the V11() ext-real real Element of a, the V11() ext-real real Element of a] is set

{ the V11() ext-real real Element of a, the V11() ext-real real Element of a} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set

{ the V11() ext-real real Element of a} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set

{{ the V11() ext-real real Element of a, the V11() ext-real real Element of a},{ the V11() ext-real real Element of a}} is non empty finite V48() set

M . [ the V11() ext-real real Element of a, the V11() ext-real real Element of a] is set

x1 is set

y1 is V11() ext-real real Element of a

M . (y1,y1) is V11() ext-real real Element of REAL

[y1,y1] is set

{y1,y1} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set

{y1} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set

{{y1,y1},{y1}} is non empty finite V48() set

M . [y1,y1] is set

[x1,x1] is set

{x1,x1} is non empty finite set

{x1} is non empty finite set

{{x1,x1},{x1}} is non empty finite V48() set

(a,M,x) is Relation-like a -defined a -valued finite Element of bool [:a,a:]

y is V11() ext-real non negative real set

(a,M,y) is Relation-like a -defined a -valued finite Element of bool [:a,a:]

(a,M,y) [*] is Relation-like a -defined a -valued finite Element of bool [:a,a:]

x1 is Relation-like a -defined a -valued total symmetric transitive finite Element of bool [:a,a:]

Class x1 is non empty with_non-empty_elements finite V48() a_partition of a

a is non empty set

[:a,a:] is non empty set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]

(a,M) is Element of bool (PARTITIONS a)

PARTITIONS a is set

bool (PARTITIONS a) is non empty set

R is non empty with_non-empty_elements a_partition of a

x is non empty with_non-empty_elements a_partition of a

bool [:a,a:] is non empty set

x1 is Relation-like a -defined a -valued total symmetric transitive Element of bool [:a,a:]

y is V11() ext-real non negative real set

(a,M,y) is Relation-like a -defined a -valued Element of bool [:a,a:]

(a,M,y) [*] is Relation-like a -defined a -valued Element of bool [:a,a:]

Class x1 is non empty with_non-empty_elements a_partition of a

d1 is Relation-like a -defined a -valued total symmetric transitive Element of bool [:a,a:]

y1 is V11() ext-real non negative real set

(a,M,y1) is Relation-like a -defined a -valued Element of bool [:a,a:]

(a,M,y1) [*] is Relation-like a -defined a -valued Element of bool [:a,a:]

Class d1 is non empty with_non-empty_elements a_partition of a

y is set

c is set

Class (x1,c) is Element of bool a

bool a is non empty set

Class (d1,c) is Element of bool a

x is set

x is set

y is set

c is set

Class (d1,c) is Element of bool a

bool a is non empty set

Class (x1,c) is Element of bool a

x is set

x is set

a is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

[:a,a:] is non empty finite set

[:[:a,a:],REAL:] is non empty set

bool [:[:a,a:],REAL:] is non empty set

%I a is non empty with_non-empty_elements finite V48() a_partition of a

id a is non empty Relation-like a -defined a -valued total finite Element of bool [:a,a:]

bool [:a,a:] is non empty finite V48() set

Class (id a) is non empty with_non-empty_elements finite V48() a_partition of a

M is Relation-like [:a,a:] -defined REAL -valued Function-like V29([:a,a:], REAL ) finite Element of bool [:[:a,a:],REAL:]

(a,M) is Element of bool (PARTITIONS a)

PARTITIONS a is set

bool (PARTITIONS a) is non empty set

{a} is non empty finite V48() set

a is MetrStruct

the carrier of a is set

a is non empty MetrStruct

the carrier of a is non empty set

[: the carrier of a, the carrier of a:] is non empty set

bool [: the carrier of a, the carrier of a:] is non empty set

M is V11() ext-real real set

R is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

x is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

y is Element of the carrier of a

x1 is Element of the carrier of a

[y,x1] is set

{y,x1} is non empty finite set

{y} is non empty finite set

{{y,x1},{y}} is non empty finite V48() set

y1 is Element of the carrier of a

d1 is Element of the carrier of a

[y1,d1] is set

{y1,d1} is non empty finite set

{y1} is non empty finite set

{{y1,d1},{y1}} is non empty finite V48() set

R is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

x is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

y is set

x1 is set

[y,x1] is set

{y,x1} is non empty finite set

{y} is non empty finite set

{{y,x1},{y}} is non empty finite V48() set

y1 is Element of the carrier of a

d1 is Element of the carrier of a

y is set

x1 is set

[y,x1] is set

{y,x1} is non empty finite set

{y} is non empty finite set

{{y,x1},{y}} is non empty finite V48() set

y1 is Element of the carrier of a

d1 is Element of the carrier of a

a is non empty MetrStruct

the carrier of a is non empty set

the distance of a is Relation-like [: the carrier of a, the carrier of a:] -defined REAL -valued Function-like V29([: the carrier of a, the carrier of a:], REAL ) Element of bool [:[: the carrier of a, the carrier of a:],REAL:]

[: the carrier of a, the carrier of a:] is non empty set

[:[: the carrier of a, the carrier of a:],REAL:] is non empty set

bool [:[: the carrier of a, the carrier of a:],REAL:] is non empty set

M is V11() ext-real real set

(a,M) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

bool [: the carrier of a, the carrier of a:] is non empty set

( the carrier of a, the distance of a,M) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

R is set

x is set

y is set

[x,y] is set

{x,y} is non empty finite set

{x} is non empty finite set

{{x,y},{x}} is non empty finite V48() set

x1 is Element of the carrier of a

y1 is Element of the carrier of a

dist (x1,y1) is V11() ext-real real Element of REAL

the distance of a . (x1,y1) is V11() ext-real real Element of REAL

[x1,y1] is set

{x1,y1} is non empty finite set

{x1} is non empty finite set

{{x1,y1},{x1}} is non empty finite V48() set

the distance of a . [x1,y1] is set

R is set

x is set

y is set

[x,y] is set

{x,y} is non empty finite set

{x} is non empty finite set

{{x,y},{x}} is non empty finite V48() set

x1 is Element of the carrier of a

y1 is Element of the carrier of a

the distance of a . (x1,y1) is V11() ext-real real Element of REAL

[x1,y1] is set

{x1,y1} is non empty finite set

{x1} is non empty finite set

{{x1,y1},{x1}} is non empty finite V48() set

the distance of a . [x1,y1] is set

dist (x1,y1) is V11() ext-real real Element of REAL

a is non empty Reflexive symmetric MetrStruct

the carrier of a is non empty set

[: the carrier of a, the carrier of a:] is non empty set

bool [: the carrier of a, the carrier of a:] is non empty set

M is V11() ext-real real set

(a,M) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

R is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

the distance of a is Relation-like [: the carrier of a, the carrier of a:] -defined REAL -valued Function-like V29([: the carrier of a, the carrier of a:], REAL ) Element of bool [:[: the carrier of a, the carrier of a:],REAL:]

[:[: the carrier of a, the carrier of a:],REAL:] is non empty set

bool [:[: the carrier of a, the carrier of a:],REAL:] is non empty set

( the carrier of a, the distance of a,M) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

a is non empty Reflexive symmetric MetrStruct

the carrier of a is non empty set

PARTITIONS the carrier of a is set

bool (PARTITIONS the carrier of a) is non empty set

[: the carrier of a, the carrier of a:] is non empty set

bool [: the carrier of a, the carrier of a:] is non empty set

M is set

R is set

R is Element of bool (PARTITIONS the carrier of a)

x is set

x1 is Relation-like the carrier of a -defined the carrier of a -valued total symmetric transitive Element of bool [: the carrier of a, the carrier of a:]

y is V11() ext-real non negative real set

(a,y) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

(a,y) [*] is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

Class x1 is non empty with_non-empty_elements a_partition of the carrier of a

M is Element of bool (PARTITIONS the carrier of a)

R is Element of bool (PARTITIONS the carrier of a)

a is non empty Reflexive symmetric MetrStruct

(a) is Element of bool (PARTITIONS the carrier of a)

the carrier of a is non empty set

PARTITIONS the carrier of a is set

bool (PARTITIONS the carrier of a) is non empty set

the distance of a is Relation-like [: the carrier of a, the carrier of a:] -defined REAL -valued Function-like V29([: the carrier of a, the carrier of a:], REAL ) Element of bool [:[: the carrier of a, the carrier of a:],REAL:]

[: the carrier of a, the carrier of a:] is non empty set

[:[: the carrier of a, the carrier of a:],REAL:] is non empty set

bool [:[: the carrier of a, the carrier of a:],REAL:] is non empty set

( the carrier of a, the distance of a) is Element of bool (PARTITIONS the carrier of a)

M is set

bool [: the carrier of a, the carrier of a:] is non empty set

x is Relation-like the carrier of a -defined the carrier of a -valued total symmetric transitive Element of bool [: the carrier of a, the carrier of a:]

R is V11() ext-real non negative real set

( the carrier of a, the distance of a,R) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

( the carrier of a, the distance of a,R) [*] is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

Class x is non empty with_non-empty_elements a_partition of the carrier of a

y is Relation-like the carrier of a -defined the carrier of a -valued total symmetric transitive Element of bool [: the carrier of a, the carrier of a:]

(a,R) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

(a,R) [*] is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

M is set

x is Relation-like the carrier of a -defined the carrier of a -valued total symmetric transitive Element of bool [: the carrier of a, the carrier of a:]

R is V11() ext-real non negative real set

(a,R) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

(a,R) [*] is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

Class x is non empty with_non-empty_elements a_partition of the carrier of a

( the carrier of a, the distance of a,R) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

( the carrier of a, the distance of a,R) [*] is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

a is non empty Reflexive discerning symmetric triangle MetrStruct

the carrier of a is non empty set

[: the carrier of a, the carrier of a:] is non empty set

bool [: the carrier of a, the carrier of a:] is non empty set

(a,0) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

(a,0) [*] is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

%I the carrier of a is non empty with_non-empty_elements a_partition of the carrier of a

id the carrier of a is non empty Relation-like the carrier of a -defined the carrier of a -valued total Element of bool [: the carrier of a, the carrier of a:]

Class (id the carrier of a) is non empty with_non-empty_elements a_partition of the carrier of a

M is Element of the carrier of a

R is Element of the carrier of a

dist (M,R) is V11() ext-real real Element of REAL

the distance of a is Relation-like [: the carrier of a, the carrier of a:] -defined REAL -valued Function-like V29([: the carrier of a, the carrier of a:], REAL ) Element of bool [:[: the carrier of a, the carrier of a:],REAL:]

[:[: the carrier of a, the carrier of a:],REAL:] is non empty set

bool [:[: the carrier of a, the carrier of a:],REAL:] is non empty set

the distance of a . (M,R) is V11() ext-real real Element of REAL

[M,R] is set

{M,R} is non empty finite set

{M} is non empty finite set

{{M,R},{M}} is non empty finite V48() set

the distance of a . [M,R] is set

M is Relation-like the carrier of a -defined the carrier of a -valued total symmetric transitive Element of bool [: the carrier of a, the carrier of a:]

Class M is non empty with_non-empty_elements a_partition of the carrier of a

( the carrier of a, the distance of a,0) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

( the carrier of a, the distance of a,0) [*] is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

a is V11() ext-real real set

M is non empty Reflexive symmetric bounded MetrStruct

[#] M is non empty non proper bounded Element of bool the carrier of M

the carrier of M is non empty set

bool the carrier of M is non empty set

diameter ([#] M) is V11() ext-real real Element of REAL

(M,a) is Relation-like the carrier of M -defined the carrier of M -valued Element of bool [: the carrier of M, the carrier of M:]

[: the carrier of M, the carrier of M:] is non empty set

bool [: the carrier of M, the carrier of M:] is non empty set

nabla the carrier of M is Relation-like the carrier of M -defined the carrier of M -valued total reflexive symmetric transitive Element of bool [: the carrier of M, the carrier of M:]

R is set

x is set

y is set

[x,y] is set

{x,y} is non empty finite set

{x} is non empty finite set

{{x,y},{x}} is non empty finite V48() set

x1 is Element of the carrier of M

y1 is Element of the carrier of M

dist (x1,y1) is V11() ext-real real Element of REAL

a is V11() ext-real real set

M is non empty Reflexive symmetric bounded MetrStruct

[#] M is non empty non proper bounded Element of bool the carrier of M

the carrier of M is non empty set

bool the carrier of M is non empty set

diameter ([#] M) is V11() ext-real real Element of REAL

(M,a) is Relation-like the carrier of M -defined the carrier of M -valued Element of bool [: the carrier of M, the carrier of M:]

[: the carrier of M, the carrier of M:] is non empty set

bool [: the carrier of M, the carrier of M:] is non empty set

(M,a) [*] is Relation-like the carrier of M -defined the carrier of M -valued Element of bool [: the carrier of M, the carrier of M:]

nabla the carrier of M is Relation-like the carrier of M -defined the carrier of M -valued total reflexive symmetric transitive Element of bool [: the carrier of M, the carrier of M:]

a is V11() ext-real real set

M is non empty Reflexive symmetric bounded MetrStruct

[#] M is non empty non proper bounded Element of bool the carrier of M

the carrier of M is non empty set

bool the carrier of M is non empty set

diameter ([#] M) is V11() ext-real real Element of REAL

(M,a) is Relation-like the carrier of M -defined the carrier of M -valued Element of bool [: the carrier of M, the carrier of M:]

[: the carrier of M, the carrier of M:] is non empty set

bool [: the carrier of M, the carrier of M:] is non empty set

(M,a) [*] is Relation-like the carrier of M -defined the carrier of M -valued Element of bool [: the carrier of M, the carrier of M:]

nabla the carrier of M is Relation-like the carrier of M -defined the carrier of M -valued total reflexive symmetric transitive Element of bool [: the carrier of M, the carrier of M:]

a is non empty Reflexive symmetric bounded MetrStruct

the carrier of a is non empty set

[: the carrier of a, the carrier of a:] is non empty set

bool [: the carrier of a, the carrier of a:] is non empty set

[#] a is non empty non proper bounded Element of bool the carrier of a

bool the carrier of a is non empty set

diameter ([#] a) is V11() ext-real real Element of REAL

{ the carrier of a} is non empty finite set

M is Relation-like the carrier of a -defined the carrier of a -valued total symmetric transitive Element of bool [: the carrier of a, the carrier of a:]

Class M is non empty with_non-empty_elements a_partition of the carrier of a

R is V11() ext-real non negative real set

(a,R) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

(a,R) [*] is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

nabla the carrier of a is Relation-like the carrier of a -defined the carrier of a -valued total reflexive symmetric transitive Element of bool [: the carrier of a, the carrier of a:]

Class (nabla the carrier of a) is non empty with_non-empty_elements a_partition of the carrier of a

a is non empty Reflexive symmetric triangle MetrStruct

the carrier of a is non empty set

bool the carrier of a is non empty set

M is non empty bounded Element of bool the carrier of a

diameter M is V11() ext-real real Element of REAL

a is non empty Reflexive discerning symmetric triangle bounded MetrStruct

the carrier of a is non empty set

{ the carrier of a} is non empty finite set

(a) is Element of bool (PARTITIONS the carrier of a)

PARTITIONS the carrier of a is set

bool (PARTITIONS the carrier of a) is non empty set

[#] a is non empty non proper bounded Element of bool the carrier of a

bool the carrier of a is non empty set

diameter ([#] a) is V11() ext-real non negative real Element of REAL

the distance of a is Relation-like [: the carrier of a, the carrier of a:] -defined REAL -valued Function-like V29([: the carrier of a, the carrier of a:], REAL ) Element of bool [:[: the carrier of a, the carrier of a:],REAL:]

[: the carrier of a, the carrier of a:] is non empty set

[:[: the carrier of a, the carrier of a:],REAL:] is non empty set

bool [:[: the carrier of a, the carrier of a:],REAL:] is non empty set

( the carrier of a, the distance of a,(diameter ([#] a))) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

bool [: the carrier of a, the carrier of a:] is non empty set

(a,(diameter ([#] a))) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

(a,(diameter ([#] a))) [*] is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

R is Relation-like the carrier of a -defined the carrier of a -valued total symmetric transitive Element of bool [: the carrier of a, the carrier of a:]

Class R is non empty with_non-empty_elements a_partition of the carrier of a

a is non empty Reflexive symmetric MetrStruct

(a) is Element of bool (PARTITIONS the carrier of a)

the carrier of a is non empty set

PARTITIONS the carrier of a is set

bool (PARTITIONS the carrier of a) is non empty set

the distance of a is Relation-like [: the carrier of a, the carrier of a:] -defined REAL -valued Function-like V29([: the carrier of a, the carrier of a:], REAL ) Element of bool [:[: the carrier of a, the carrier of a:],REAL:]

[: the carrier of a, the carrier of a:] is non empty set

[:[: the carrier of a, the carrier of a:],REAL:] is non empty set

bool [:[: the carrier of a, the carrier of a:],REAL:] is non empty set

( the carrier of a, the distance of a) is Element of bool (PARTITIONS the carrier of a)

M is non empty Reflexive discerning symmetric triangle bounded MetrStruct

(M) is Element of bool (PARTITIONS the carrier of M)

the carrier of M is non empty set

PARTITIONS the carrier of M is set

bool (PARTITIONS the carrier of M) is non empty set

the distance of M is Relation-like [: the carrier of M, the carrier of M:] -defined REAL -valued Function-like V29([: the carrier of M, the carrier of M:], REAL ) Element of bool [:[: the carrier of M, the carrier of M:],REAL:]

[: the carrier of M, the carrier of M:] is non empty set

[:[: the carrier of M, the carrier of M:],REAL:] is non empty set

bool [:[: the carrier of M, the carrier of M:],REAL:] is non empty set

a is V11() ext-real non negative real set

( the carrier of M, the distance of M,a) is Relation-like the carrier of M -defined the carrier of M -valued Element of bool [: the carrier of M, the carrier of M:]

bool [: the carrier of M, the carrier of M:] is non empty set

(M,a) is Relation-like the carrier of M -defined the carrier of M -valued Element of bool [: the carrier of M, the carrier of M:]

(M,a) [*] is Relation-like the carrier of M -defined the carrier of M -valued Element of bool [: the carrier of M, the carrier of M:]

R is Relation-like the carrier of M -defined the carrier of M -valued total symmetric transitive Element of bool [: the carrier of M, the carrier of M:]

Class R is non empty with_non-empty_elements a_partition of the carrier of M

%I the carrier of M is non empty with_non-empty_elements a_partition of the carrier of M

id the carrier of M is non empty Relation-like the carrier of M -defined the carrier of M -valued total Element of bool [: the carrier of M, the carrier of M:]

Class (id the carrier of M) is non empty with_non-empty_elements a_partition of the carrier of M

{ the carrier of M} is non empty finite set