:: PARTIT_2 semantic presentation

K128() is Element of bool K124()

K124() is set

bool K124() is non empty set

K123() is set

bool K123() is non empty set

bool K128() is non empty set

BOOLEAN is non empty set

1 is non empty set

[:1,1:] is non empty Relation-like set

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

[:[:1,1:],1:] is non empty Relation-like set

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

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() set

the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() set

TRUE is boolean Element of BOOLEAN

FALSE is boolean Element of BOOLEAN

K129() is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() Element of K128()

field {} is set

K174() is set

K175() is set

{{}} is non empty functional set

X is non empty set

PARTITIONS X is non empty partition-membered Element of bool (bool (bool X))

bool X is non empty Element of bool (bool X)

bool X is non empty set

bool (bool X) is non empty set

bool (bool X) is non empty set

bool (bool (bool X)) is non empty set

bool (PARTITIONS X) is non empty set

f is non empty Element of bool (PARTITIONS X)

a is Element of f

X is non empty set

PARTITIONS X is non empty partition-membered Element of bool (bool (bool X))

bool X is non empty Element of bool (bool X)

bool X is non empty set

bool (bool X) is non empty set

bool (bool X) is non empty set

bool (bool (bool X)) is non empty set

{} (PARTITIONS X) is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() Element of bool (PARTITIONS X)

bool (PARTITIONS X) is non empty set

'/\' ({} (PARTITIONS X)) is non empty with_non-empty_elements a_partition of X

%O X is non empty with_non-empty_elements a_partition of X

f is set

{X} is non empty set

a is Relation-like Function-like set

{} (bool X) is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() Element of bool (bool X)

x is Relation-like Function-like set

dom x is set

rng x is set

y is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() Element of bool (bool X)

z is set

x . z is set

Intersect y is Element of bool X

a is Relation-like Function-like set

dom a is set

rng a is set

x is Element of bool (bool X)

Intersect x is Element of bool X

X is non empty set

[:X,X:] is non empty Relation-like set

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

f is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

a is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

f \/ a is Relation-like X -defined X -valued Element of bool [:X,X:]

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

x is Element of X

y is Element of X

[x,y] is set

{x,y} is non empty set

{x} is non empty set

{{x,y},{x}} is non empty set

[y,y] is set

{y,y} is non empty set

{y} is non empty set

{{y,y},{y}} is non empty set

[x,x] is set

{x,x} is non empty set

{{x,x},{x}} is non empty set

X is non empty set

[:X,X:] is non empty Relation-like set

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

f is Relation-like X -defined X -valued Element of bool [:X,X:]

nabla X is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

X is non empty set

[:X,X:] is non empty Relation-like set

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

nabla X is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

f is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

(nabla X) * f is Relation-like X -defined X -valued Element of bool [:X,X:]

f * (nabla X) is Relation-like X -defined X -valued Element of bool [:X,X:]

(nabla X) \/ f is Relation-like X -defined X -valued Element of bool [:X,X:]

X is non empty set

f is non empty with_non-empty_elements a_partition of X

ERl f is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

[:X,X:] is non empty Relation-like set

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

a is Element of X

x is Element of X

[a,x] is set

{a,x} is non empty set

{a} is non empty set

{{a,x},{a}} is non empty set

EqClass (x,f) is Element of f

bool X is non empty set

y is Element of bool X

X is non empty set

x is non empty with_non-empty_elements a_partition of X

ERl x is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

[:X,X:] is non empty Relation-like set

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

f is non empty with_non-empty_elements a_partition of X

ERl f is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

a is non empty with_non-empty_elements a_partition of X

ERl a is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

(ERl f) * (ERl a) is Relation-like X -defined X -valued Element of bool [:X,X:]

y is Element of X

z is Element of X

EqClass (z,x) is Element of x

EqClass (z,a) is Element of a

[y,z] is set

{y,z} is non empty set

{y} is non empty set

{{y,z},{y}} is non empty set

B is Element of X

[y,B] is set

{y,B} is non empty set

{{y,B},{y}} is non empty set

[B,z] is set

{B,z} is non empty set

{B} is non empty set

{{B,z},{B}} is non empty set

x is Element of X

EqClass (x,f) is Element of f

B is Element of X

EqClass (B,f) is Element of f

[y,B] is set

{y,B} is non empty set

{{y,B},{y}} is non empty set

[B,z] is set

{B,z} is non empty set

{B} is non empty set

{{B,z},{B}} is non empty set

X is Relation-like set

f is Relation-like set

X * f is Relation-like set

a is set

x is set

[x,x] is set

{x,x} is non empty set

{x} is non empty set

{{x,x},{x}} is non empty set

X is Relation-like set

field X is set

f is set

a is set

[a,a] is set

{a,a} is non empty set

{a} is non empty set

{{a,a},{a}} is non empty set

X is set

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

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

f is Relation-like X -defined X -valued Element of bool [:X,X:]

field f is set

X \/ X is set

X is non empty set

[:X,X:] is non empty Relation-like set

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

f is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

a is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

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

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

field a is set

field f is set

field (f * a) is set

dom (f * a) is Element of bool X

bool X is non empty set

x is set

y is set

[x,y] is set

{x,y} is non empty set

{x} is non empty set

{{x,y},{x}} is non empty set

[y,x] is set

{y,x} is non empty set

{y} is non empty set

{{y,x},{y}} is non empty set

z is set

[x,z] is set

{x,z} is non empty set

{{x,z},{x}} is non empty set

[z,y] is set

{z,y} is non empty set

{z} is non empty set

{{z,y},{z}} is non empty set

[y,z] is set

{y,z} is non empty set

{{y,z},{y}} is non empty set

[z,x] is set

{z,x} is non empty set

{{z,x},{z}} is non empty set

f * f is Relation-like X -defined X -valued Element of bool [:X,X:]

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

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

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

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

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

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

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

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

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

X is non empty set

[:X,BOOLEAN:] is non empty Relation-like set

bool [:X,BOOLEAN:] is non empty set

f is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

a is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' a is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' f is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

x is Element of X

('not' a) . x is boolean Element of BOOLEAN

('not' f) . x is boolean Element of BOOLEAN

a . x is boolean Element of BOOLEAN

'not' ('not' a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

('not' ('not' a)) . x is boolean Element of BOOLEAN

'not' TRUE is boolean Element of BOOLEAN

K105(1,TRUE) is set

f . x is boolean Element of BOOLEAN

'not' FALSE is boolean Element of BOOLEAN

K105(1,FALSE) is set

X is non empty set

[:X,BOOLEAN:] is non empty Relation-like set

bool [:X,BOOLEAN:] is non empty set

PARTITIONS X is non empty partition-membered Element of bool (bool (bool X))

bool X is non empty Element of bool (bool X)

bool X is non empty set

bool (bool X) is non empty set

bool (bool X) is non empty set

bool (bool (bool X)) is non empty set

bool (PARTITIONS X) is non empty set

f is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

a is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

x is Element of bool (PARTITIONS X)

y is non empty with_non-empty_elements a_partition of X

All (f,y,x) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

All (a,y,x) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

z is Element of X

(All (f,y,x)) . z is boolean Element of BOOLEAN

(All (a,y,x)) . z is boolean Element of BOOLEAN

CompF (y,x) is non empty with_non-empty_elements a_partition of X

B_INF (f,(CompF (y,x))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

EqClass (z,(CompF (y,x))) is Element of CompF (y,x)

B is Element of X

a . B is boolean Element of BOOLEAN

f . B is boolean Element of BOOLEAN

B_INF (a,(CompF (y,x))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

X is non empty set

[:X,BOOLEAN:] is non empty Relation-like set

bool [:X,BOOLEAN:] is non empty set

PARTITIONS X is non empty partition-membered Element of bool (bool (bool X))

bool X is non empty Element of bool (bool X)

bool X is non empty set

bool (bool X) is non empty set

bool (bool X) is non empty set

bool (bool (bool X)) is non empty set

bool (PARTITIONS X) is non empty set

f is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

a is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

x is Element of bool (PARTITIONS X)

y is non empty with_non-empty_elements a_partition of X

Ex (f,y,x) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

Ex (a,y,x) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' a is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' ('not' a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

Ex (('not' ('not' a)),y,x) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

All (('not' a),y,x) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' (All (('not' a),y,x)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' f is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

All (('not' f),y,x) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' ('not' f) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

Ex (('not' ('not' f)),y,x) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' (All (('not' f),y,x)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

X is non empty set

PARTITIONS X is non empty partition-membered Element of bool (bool (bool X))

bool X is non empty Element of bool (bool X)

bool X is non empty set

bool (bool X) is non empty set

bool (bool X) is non empty set

bool (bool (bool X)) is non empty set

bool (PARTITIONS X) is non empty set

f is Element of bool (PARTITIONS X)

a is Element of bool (PARTITIONS X)

x is Element of bool (PARTITIONS X)

'/\' a is non empty with_non-empty_elements a_partition of X

ERl ('/\' a) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

[:X,X:] is non empty Relation-like set

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

'/\' x is non empty with_non-empty_elements a_partition of X

ERl ('/\' x) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

(ERl ('/\' a)) * (ERl ('/\' x)) is Relation-like X -defined X -valued Element of bool [:X,X:]

(ERl ('/\' x)) * (ERl ('/\' a)) is Relation-like X -defined X -valued Element of bool [:X,X:]

{} (PARTITIONS X) is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() Element of bool (PARTITIONS X)

%O X is non empty with_non-empty_elements a_partition of X

ERl (%O X) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

(ERl ('/\' x)) * (ERl (%O X)) is Relation-like X -defined X -valued Element of bool [:X,X:]

nabla X is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

(ERl ('/\' x)) * (nabla X) is Relation-like X -defined X -valued Element of bool [:X,X:]

{} (PARTITIONS X) is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() Element of bool (PARTITIONS X)

%O X is non empty with_non-empty_elements a_partition of X

ERl (%O X) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

(ERl (%O X)) * (ERl ('/\' a)) is Relation-like X -defined X -valued Element of bool [:X,X:]

nabla X is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

(nabla X) * (ERl ('/\' a)) is Relation-like X -defined X -valued Element of bool [:X,X:]

z is Element of X

B is Element of X

[z,B] is set

{z,B} is non empty set

{z} is non empty set

{{z,B},{z}} is non empty set

x is Element of X

[z,x] is set

{z,x} is non empty set

{{z,x},{z}} is non empty set

[x,B] is set

{x,B} is non empty set

{x} is non empty set

{{x,B},{x}} is non empty set

z is Element of bool X

y is Element of bool X

u is Relation-like Function-like set

dom u is set

rng u is set

u is Element of bool (bool X)

Intersect u is Element of bool X

hP is Relation-like Function-like set

dom hP is set

rng hP is set

FP is Element of bool (bool X)

Intersect FP is Element of bool X

P is non empty Element of bool (PARTITIONS X)

[:P,(bool X):] is non empty Relation-like set

bool [:P,(bool X):] is non empty set

hP9 is non empty Relation-like P -defined bool X -valued Function-like V17(P) quasi_total Element of bool [:P,(bool X):]

Q is non empty Element of bool (PARTITIONS X)

[:Q,(bool X):] is non empty Relation-like set

bool [:Q,(bool X):] is non empty set

hQ9 is non empty Relation-like Q -defined bool X -valued Function-like V17(Q) quasi_total Element of bool [:Q,(bool X):]

y is non empty Element of bool (PARTITIONS X)

h9 is non empty with_non-empty_elements (X,y)

[:y,(bool X):] is non empty Relation-like set

bool [:y,(bool X):] is non empty set

h9 is non empty Relation-like y -defined bool X -valued Function-like V17(y) quasi_total Element of bool [:y,(bool X):]

h9 +* hP9 is Relation-like Function-like set

(h9 +* hP9) +* hQ9 is Relation-like Function-like set

dom hQ9 is non empty Element of bool Q

bool Q is non empty set

dom hP9 is non empty Element of bool P

bool P is non empty set

FP9 is set

((h9 +* hP9) +* hQ9) . FP9 is set

hP9 . FP9 is set

u . FP9 is set

hP . FP9 is set

hQ9 . FP9 is set

FQ9 is non empty with_non-empty_elements (X,P)

EqClass (z,FQ9) is Element of FQ9

EqClass (x,FQ9) is Element of FQ9

EqClass (B,FQ9) is Element of FQ9

(h9 +* hP9) . FP9 is set

rng hP9 is non empty Element of bool (bool X)

rng hQ9 is non empty Element of bool (bool X)

FP9 is Element of bool (bool X)

Intersect FP9 is Element of bool X

FQ9 is Element of bool (bool X)

Intersect FQ9 is Element of bool X

F is set

t is set

hP9 . t is set

a is non empty with_non-empty_elements (X,P)

EqClass (B,a) is Element of a

F is set

t is set

hQ9 . t is set

a is non empty with_non-empty_elements (X,Q)

EqClass (z,a) is Element of a

F is set

hQ9 . F is set

t is non empty with_non-empty_elements (X,Q)

hQ9 . t is Element of bool X

EqClass (z,t) is Element of t

rng (h9 +* hP9) is set

rng h9 is non empty Element of bool (bool X)

(rng h9) \/ (rng hP9) is non empty Element of bool (bool X)

rng ((h9 +* hP9) +* hQ9) is set

(rng (h9 +* hP9)) \/ (rng hQ9) is non empty set

dom ((h9 +* hP9) +* hQ9) is set

dom (h9 +* hP9) is set

(dom (h9 +* hP9)) \/ Q is non empty set

dom h9 is non empty Element of bool y

bool y is non empty set

(dom h9) \/ P is non empty set

((dom h9) \/ P) \/ Q is non empty set

f \/ P is non empty Element of bool (PARTITIONS X)

(f \/ P) \/ Q is non empty Element of bool (PARTITIONS X)

f \/ Q is non empty Element of bool (PARTITIONS X)

t is set

hP9 . t is set

a is non empty with_non-empty_elements (X,P)

hP9 . a is Element of bool X

EqClass (B,a) is Element of a

t is set

((h9 +* hP9) +* hQ9) . t is set

P \/ Q is non empty Element of bool (PARTITIONS X)

(P \/ Q) \/ f is non empty Element of bool (PARTITIONS X)

f \ (P \/ Q) is Element of bool (PARTITIONS X)

(f \ (P \/ Q)) \/ (P \/ Q) is non empty Element of bool (PARTITIONS X)

hQ9 . t is set

hP9 . t is set

hP9 +* hQ9 is Relation-like Function-like set

h9 +* (hP9 +* hQ9) is Relation-like Function-like set

dom (hP9 +* hQ9) is set

h9 . t is set

F is Element of bool (bool X)

Intersect F is Element of bool X

t is Element of X

a is set

b is set

hP9 . b is set

((h9 +* hP9) +* hQ9) . b is set

'/\' P is non empty with_non-empty_elements a_partition of X

[t,B] is set

{t,B} is non empty set

{t} is non empty set

{{t,B},{t}} is non empty set

ERl ('/\' P) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

a is set

b is set

hQ9 . b is set

b is non empty with_non-empty_elements (X,Q)

hQ9 . b is Element of bool X

((h9 +* hP9) +* hQ9) . b is set

'/\' Q is non empty with_non-empty_elements a_partition of X

[z,t] is set

{z,t} is non empty set

{{z,t},{z}} is non empty set

ERl ('/\' Q) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

X is non empty set

PARTITIONS X is non empty partition-membered Element of bool (bool (bool X))

bool X is non empty Element of bool (bool X)

bool X is non empty set

bool (bool X) is non empty set

bool (bool X) is non empty set

bool (bool (bool X)) is non empty set

bool (PARTITIONS X) is non empty set

f is Element of bool (PARTITIONS X)

a is Element of bool (PARTITIONS X)

x is Element of bool (PARTITIONS X)

'/\' a is non empty with_non-empty_elements a_partition of X

ERl ('/\' a) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

[:X,X:] is non empty Relation-like set

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

'/\' x is non empty with_non-empty_elements a_partition of X

ERl ('/\' x) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

(ERl ('/\' a)) * (ERl ('/\' x)) is Relation-like X -defined X -valued Element of bool [:X,X:]

(ERl ('/\' x)) * (ERl ('/\' a)) is Relation-like X -defined X -valued Element of bool [:X,X:]

X is non empty set

[:X,BOOLEAN:] is non empty Relation-like set

bool [:X,BOOLEAN:] is non empty set

PARTITIONS X is non empty partition-membered Element of bool (bool (bool X))

bool X is non empty Element of bool (bool X)

bool X is non empty set

bool (bool X) is non empty set

bool (bool X) is non empty set

bool (bool (bool X)) is non empty set

bool (PARTITIONS X) is non empty set

f is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

a is Element of bool (PARTITIONS X)

x is non empty with_non-empty_elements a_partition of X

All (f,x,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

y is non empty with_non-empty_elements a_partition of X

All ((All (f,x,a)),y,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

All (f,y,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

All ((All (f,y,a)),x,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

{x} is non empty Element of bool (PARTITIONS X)

a \ {x} is Element of bool (PARTITIONS X)

{y} is non empty Element of bool (PARTITIONS X)

a \ {y} is Element of bool (PARTITIONS X)

CompF (x,a) is non empty with_non-empty_elements a_partition of X

'/\' (a \ {x}) is non empty with_non-empty_elements a_partition of X

CompF (y,a) is non empty with_non-empty_elements a_partition of X

'/\' (a \ {y}) is non empty with_non-empty_elements a_partition of X

ERl ('/\' (a \ {x})) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

[:X,X:] is non empty Relation-like set

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

ERl ('/\' (a \ {y})) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

(ERl ('/\' (a \ {x}))) * (ERl ('/\' (a \ {y}))) is Relation-like X -defined X -valued Element of bool [:X,X:]

(ERl ('/\' (a \ {y}))) * (ERl ('/\' (a \ {x}))) is Relation-like X -defined X -valued Element of bool [:X,X:]

B_INF (f,(CompF (x,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

B_INF (f,(CompF (y,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

B_INF ((B_INF (f,(CompF (y,a)))),(CompF (x,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

x is Element of X

EqClass (x,(CompF (y,a))) is Element of CompF (y,a)

(B_INF ((B_INF (f,(CompF (y,a)))),(CompF (x,a)))) . x is boolean Element of BOOLEAN

EqClass (x,(CompF (x,a))) is Element of CompF (x,a)

z is Element of X

(B_INF (f,(CompF (y,a)))) . z is boolean Element of BOOLEAN

[z,x] is set

{z,x} is non empty set

{z} is non empty set

{{z,x},{z}} is non empty set

EqClass (z,(CompF (y,a))) is Element of CompF (y,a)

y is Element of X

f . y is boolean Element of BOOLEAN

[y,z] is set

{y,z} is non empty set

{y} is non empty set

{{y,z},{y}} is non empty set

[y,x] is set

{y,x} is non empty set

{{y,x},{y}} is non empty set

u is set

[y,u] is set

{y,u} is non empty set

{{y,u},{y}} is non empty set

[u,x] is set

{u,x} is non empty set

{u} is non empty set

{{u,x},{u}} is non empty set

field (ERl ('/\' (a \ {y}))) is set

u is Element of X

(B_INF (f,(CompF (x,a)))) . u is boolean Element of BOOLEAN

EqClass (u,(CompF (x,a))) is Element of CompF (x,a)

z is Element of X

(B_INF (f,(CompF (x,a)))) . z is boolean Element of BOOLEAN

EqClass (z,(CompF (x,a))) is Element of CompF (x,a)

y is Element of X

f . y is boolean Element of BOOLEAN

[z,x] is set

{z,x} is non empty set

{z} is non empty set

{{z,x},{z}} is non empty set

[y,z] is set

{y,z} is non empty set

{y} is non empty set

{{y,z},{y}} is non empty set

[y,x] is set

{y,x} is non empty set

{{y,x},{y}} is non empty set

u is set

[y,u] is set

{y,u} is non empty set

{{y,u},{y}} is non empty set

[u,x] is set

{u,x} is non empty set

{u} is non empty set

{{u,x},{u}} is non empty set

field (ERl ('/\' (a \ {y}))) is set

u is Element of X

EqClass (u,(CompF (y,a))) is Element of CompF (y,a)

(B_INF (f,(CompF (y,a)))) . u is boolean Element of BOOLEAN

B_INF ((All (f,x,a)),(CompF (y,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

B_INF ((B_INF (f,(CompF (x,a)))),(CompF (y,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

B_INF ((All (f,y,a)),(CompF (x,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

X is non empty set

[:X,BOOLEAN:] is non empty Relation-like set

bool [:X,BOOLEAN:] is non empty set

PARTITIONS X is non empty partition-membered Element of bool (bool (bool X))

bool X is non empty Element of bool (bool X)

bool X is non empty set

bool (bool X) is non empty set

bool (bool X) is non empty set

bool (bool (bool X)) is non empty set

bool (PARTITIONS X) is non empty set

f is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

a is Element of bool (PARTITIONS X)

x is non empty with_non-empty_elements a_partition of X

Ex (f,x,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

y is non empty with_non-empty_elements a_partition of X

Ex ((Ex (f,x,a)),y,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

Ex (f,y,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

Ex ((Ex (f,y,a)),x,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' (Ex ((Ex (f,x,a)),y,a)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' ('not' (Ex ((Ex (f,x,a)),y,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' (Ex (f,x,a)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

All (('not' (Ex (f,x,a))),y,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' (All (('not' (Ex (f,x,a))),y,a)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' f is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

All (('not' f),x,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

All ((All (('not' f),x,a)),y,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' (All ((All (('not' f),x,a)),y,a)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

All (('not' f),y,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

All ((All (('not' f),y,a)),x,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' (All ((All (('not' f),y,a)),x,a)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' (Ex (f,y,a)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

All (('not' (Ex (f,y,a))),x,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' (All (('not' (Ex (f,y,a))),x,a)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' (Ex ((Ex (f,y,a)),x,a)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

'not' ('not' (Ex ((Ex (f,y,a)),x,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

X is non empty set

[:X,BOOLEAN:] is non empty Relation-like set

bool [:X,BOOLEAN:] is non empty set

PARTITIONS X is non empty partition-membered Element of bool (bool (bool X))

bool X is non empty Element of bool (bool X)

bool X is non empty set

bool (bool X) is non empty set

bool (bool X) is non empty set

bool (bool (bool X)) is non empty set

bool (PARTITIONS X) is non empty set

f is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

a is Element of bool (PARTITIONS X)

x is non empty with_non-empty_elements a_partition of X

All (f,x,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

y is non empty with_non-empty_elements a_partition of X

Ex ((All (f,x,a)),y,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

Ex (f,y,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

All ((Ex (f,y,a)),x,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

{x} is non empty Element of bool (PARTITIONS X)

a \ {x} is Element of bool (PARTITIONS X)

{y} is non empty Element of bool (PARTITIONS X)

a \ {y} is Element of bool (PARTITIONS X)

'/\' (a \ {x}) is non empty with_non-empty_elements a_partition of X

ERl ('/\' (a \ {x})) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

[:X,X:] is non empty Relation-like set

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

'/\' (a \ {y}) is non empty with_non-empty_elements a_partition of X

ERl ('/\' (a \ {y})) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]

(ERl ('/\' (a \ {x}))) * (ERl ('/\' (a \ {y}))) is Relation-like X -defined X -valued Element of bool [:X,X:]

(ERl ('/\' (a \ {y}))) * (ERl ('/\' (a \ {x}))) is Relation-like X -defined X -valued Element of bool [:X,X:]

CompF (x,a) is non empty with_non-empty_elements a_partition of X

CompF (y,a) is non empty with_non-empty_elements a_partition of X

B_SUP ((All (f,x,a)),(CompF (y,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

x is Element of X

(Ex ((All (f,x,a)),y,a)) . x is boolean Element of BOOLEAN

(All ((Ex (f,y,a)),x,a)) . x is boolean Element of BOOLEAN

EqClass (x,(CompF (x,a))) is Element of CompF (x,a)

z is Element of X

(Ex (f,y,a)) . z is boolean Element of BOOLEAN

EqClass (x,(CompF (y,a))) is Element of CompF (y,a)

y is Element of X

(All (f,x,a)) . y is boolean Element of BOOLEAN

[z,x] is set

{z,x} is non empty set

{z} is non empty set

{{z,x},{z}} is non empty set

[x,z] is set

{x,z} is non empty set

{x} is non empty set

{{x,z},{x}} is non empty set

[y,x] is set

{y,x} is non empty set

{y} is non empty set

{{y,x},{y}} is non empty set

[y,z] is set

{y,z} is non empty set

{{y,z},{y}} is non empty set

u is set

[y,u] is set

{y,u} is non empty set

{{y,u},{y}} is non empty set

[u,z] is set

{u,z} is non empty set

{u} is non empty set

{{u,z},{u}} is non empty set

field (ERl ('/\' (a \ {y}))) is set

u is Element of X

[u,y] is set

{u,y} is non empty set

{u} is non empty set

{{u,y},{u}} is non empty set

B_INF (f,(CompF (x,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

EqClass (y,(CompF (x,a))) is Element of CompF (x,a)

f . u is boolean Element of BOOLEAN

B_SUP (f,(CompF (y,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

EqClass (z,(CompF (y,a))) is Element of CompF (y,a)

B_INF ((Ex (f,y,a)),(CompF (x,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]

X is set

f is set

[:X,f:] is Relation-like set

bool [:X,f:] is non empty set

X is set

f is set

(X,f) is Relation-like X -defined f -valued Element of bool [:X,f:]

[:X,f:] is Relation-like set

bool [:X,f:] is non empty set

X is non empty set

id X is non empty Relation-like X -defined X -valued Function-like one-to-one V17(X) reflexive symmetric antisymmetric transitive set

field (id X) is set

dom (id X) is non empty Element of bool X

bool X is non empty set

rng (id X) is non empty Element of bool X

X \/ X is non empty set

op1 is non empty Relation-like 1 -defined 1 -valued Function-like V17(1) quasi_total Element of bool [:1,1:]

[{},{}] is set

{{},{}} is non empty functional set

{{{},{}},{{}}} is non empty set

{[{},{}]} is non empty Relation-like Function-like set

dom op1 is non empty Element of bool 1

bool 1 is non empty set

op1 . {} is set

[{},(op1 . {})] is set

{{},(op1 . {})} is non empty set

{{{},(op1 . {})},{{}}} is non empty set

{[{},(op1 . {})]} is non empty Relation-like Function-like set

rng op1 is non empty Element of bool 1

{(op1 . {})} is non empty set

[:{{}},{{}}:] is non empty Relation-like set

X is set

f is set

(X,f) is empty Relation-like non-empty empty-yielding X -defined f -valued Function-like one-to-one constant functional V56() Element of bool [:X,f:]

[:X,f:] is Relation-like set

bool [:X,f:] is non empty set

field (X,f) is set

X is non empty set

[:X,X:] is non empty Relation-like set

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

f is Relation-like X -defined X -valued Element of bool [:X,X:]

field f is set

X is non empty set

[:X,X:] is non empty Relation-like set

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

f is Relation-like X -defined X -valued Element of bool [:X,X:]

a is set

field f is set

x is set

[a,x] is set

{a,x} is non empty set

{a} is non empty set

{{a,x},{a}} is non empty set

[x,a] is set

{x,a} is non empty set

{x} is non empty set

{{x,a},{x}} is non empty set

X \/ X is non empty set

X is non empty set

[:X,X:] is non empty Relation-like set

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

f is non empty set

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

field a is set

x is set

y is set

[x,y] is set

{x,y} is non empty set

{x} is non empty set

{{x,y},{x}} is non empty set

[y,x] is set

{y,x} is non empty set

{y} is non empty set

{{y,x},{y}} is non empty set

X is non empty set

[:X,X:] is non empty Relation-like set

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

f is non empty set

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

field a is set

x is set

y is set

[x,y] is set

{x,y} is non empty set

{x} is non empty set

{{x,y},{x}} is non empty set

[y,x] is set

{y,x} is non empty set

{y} is non empty set

{{y,x},{y}} is non empty set

X is non empty set

[:X,X:] is non empty Relation-like set

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

f is Relation-like X -defined X -valued Element of bool [:X,X:]

a is set

field f is set

x is set

[a,x] is set

{a,x} is non empty set

{a} is non empty set

{{a,x},{a}} is non empty set

[x,a] is set

{x,a} is non empty set

{x} is non empty set

{{x,a},{x}} is non empty set

X \/ X is non empty set

X is non empty set

[:X,X:] is non empty Relation-like set

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

f is non empty set

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

field a is set

x is set

y is set

z is set

[x,y] is set

{x,y} is non empty set

{x} is non empty set

{{x,y},{x}} is non empty set

[y,z] is set

{y,z} is non empty set

{y} is non empty set

{{y,z},{y}} is non empty set

[x,z] is set

{x,z} is non empty set

{{x,z},{x}} is non empty set

X is non empty set

[:X,X:] is non empty Relation-like set

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

f is Relation-like X -defined X -valued Element of bool [:X,X:]

a is set

field f is set

x is set

y is set

[a,x] is set

{a,x} is non empty set

{a} is non empty set

{{a,x},{a}} is non empty set

[x,y] is set

{x,y} is non empty set

{x} is non empty set

{{x,y},{x}} is non empty set

[a,y] is set

{a,y} is non empty set

{{a,y},{a}} is non empty set

X \/ X is non empty set

X is non empty set

[:X,X:] is non empty Relation-like set

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

f is non empty set

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

field a is set

x is set

y is set

[x,y] is set

{x,y} is non empty set

{x} is non empty set

{{x,y},{x}} is non empty set

[y,x] is set

{y,x} is non empty set

{y} is non empty set

{{y,x},{y}} is non empty set

X is non empty set

[:X,X:] is non empty Relation-like set

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

f is Relation-like X -defined X -valued Element of bool [:X,X:]

a is set

field f is set

x is set

[a,x] is set

{a,x} is non empty set

{a} is non empty set

{{a,x},{a}} is non empty set

[x,a] is set

{x,a} is non empty set

{x} is non empty set

{{x,a},{x}} is non empty set

X \/ X is non empty set

X is non empty set

[:X,X:] is non empty Relation-like set

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

f is non empty set

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

field a is set

x is set

[x,x] is set

{x,x} is non empty set

{x} is non empty set

{{x,x},{x}} is non empty set

f \ (field a) is Element of bool f

bool f is non empty set

(field a) \/ (f \ (field a)) is set

dom a is Element of bool X

bool X is non empty set

rng a is Element of bool X

(dom a) \/ (rng a) is Element of bool X

f \ ((dom a) \/ (rng a)) is Element of bool f

f \ (dom a) is Element of bool f

f \ (rng a) is Element of bool f

(f \ (dom a)) /\ (f \ (rng a)) is Element of bool f

X is non empty set

[:X,X:] is non empty Relation-like set

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

f is Relation-like X -defined X -valued Element of bool [:X,X:]

field f is set

X \/ X is non empty set

a is set

[a,a] is set

{a,a} is non empty set

{a} is non empty set

{{a,a},{a}} is non empty set

X is Relation-like set

field X is set

f is set

[f,f] is set

{f,f} is non empty set

{f} is non empty set

{{f,f},{f}} is non empty set

f is set

a is set

[f,a] is set

{f,a} is non empty set

{f} is non empty set

{{f,a},{f}} is non empty set

[a,f] is set

{a,f} is non empty set

{a} is non empty set

{{a,f},{a}} is non empty set

f is set

a is set

x is set

[f,a] is set

{f,a} is non empty set

{f} is non empty set

{{f,a},{f}} is non empty set

[a,x] is set

{a,x} is non empty set

{a} is non empty set

{{a,x},{a}} is non empty set

[f,x] is set

{f,x} is non empty set

{{f,x},{f}} is non empty set

X is non empty set

[:X,X:] is non empty Relation-like set

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

f is non empty Relation-like X -defined X -valued Function-like V17(X) quasi_total Element of bool [:X,X:]

dom f is non empty Element of bool X

bool X is non empty set

a is Element of X

f . a is Element of X

f . (f . a) is Element of X

a is set

dom f is non empty set

f . a is set

f . (f . a) is set

X is Element of 1

op1 . X is Element of 1

op1 . (op1 . X) is Element of 1

X is Relation-like Function-like set

X is set

id X is Relation-like X -defined X -valued Function-like one-to-one V17(X) reflexive symmetric antisymmetric transitive set

a is set

dom (id X) is set

(id X) . a is set

(id X) . ((id X) . a) is set

dom (id X) is Element of bool X

bool X is non empty set