:: 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

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 () is non empty set
f is non empty Element of bool ()
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

bool () is non empty set
'/\' ({} ()) 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

dom x is set
rng x is set

z is set
x . z is set
Intersect y is Element of bool X

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 * 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

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:]
f * () is Relation-like X -defined X -valued Element of bool [:X,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

[: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

[: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

a is non empty with_non-empty_elements a_partition of 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

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

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

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 * 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
is non empty Relation-like set
bool is non empty set

x is Element of X
() . x is boolean Element of BOOLEAN
() . x is boolean Element of BOOLEAN
a . x is boolean Element of BOOLEAN

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

K105(1,TRUE) is set
f . x is boolean Element of BOOLEAN

K105(1,FALSE) is set
X is non empty set
is non empty Relation-like set
bool 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 () is non empty set

x is Element of bool ()
y is non empty with_non-empty_elements a_partition of X

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
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 is non empty set
is non empty Relation-like set
bool 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 () is non empty set

x is Element of bool ()
y is non empty with_non-empty_elements a_partition of X

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

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

Ex (('not' ()),y,x) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool
'not' (All ((),y,x)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool
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 () is non empty set
f is Element of bool ()
a is Element of bool ()
x is Element of bool ()
'/\' a is non empty with_non-empty_elements a_partition of 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 ('/\' 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:]

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

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

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

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

(ERl (%O X)) * (ERl ('/\' a)) is Relation-like X -defined X -valued Element of bool [:X,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

dom u is set
rng u is set
u is Element of bool (bool X)
Intersect u is Element of bool X

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 ()
[: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 ()
[: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 ()
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) +* 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 ()
(f \/ P) \/ Q is non empty Element of bool ()
f \/ Q is non empty Element of bool ()
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 ()
(P \/ Q) \/ f is non empty Element of bool ()
f \ (P \/ Q) is Element of bool ()
(f \ (P \/ Q)) \/ (P \/ Q) is non empty Element of bool ()
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

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

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 () is non empty set
f is Element of bool ()
a is Element of bool ()
x is Element of bool ()
'/\' a is non empty with_non-empty_elements a_partition of 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 ('/\' 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
is non empty Relation-like set
bool 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 () is non empty set

a is Element of bool ()
x is non empty with_non-empty_elements a_partition of X

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

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} is non empty Element of bool ()
a \ {x} is Element of bool ()
{y} is non empty Element of bool ()
a \ {y} is Element of bool ()
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

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

(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
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
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 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
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
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 is non empty set
is non empty Relation-like set
bool 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 () is non empty set

a is Element of bool ()
x is non empty with_non-empty_elements a_partition of X

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

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
'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
'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

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
'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

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

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

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
'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
'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
'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 is non empty set
is non empty Relation-like set
bool 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 () is non empty set

a is Element of bool ()
x is non empty with_non-empty_elements a_partition of X

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

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} is non empty Element of bool ()
a \ {x} is Element of bool ()
{y} is non empty Element of bool ()
a \ {y} is Element of bool ()
'/\' (a \ {x}) is non empty with_non-empty_elements a_partition of 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 \ {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 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
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
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 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

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

is set
is non empty functional set
is non empty set

dom op1 is non empty Element of bool 1
bool 1 is non empty set

[{},()] is set
{{},()} is non empty set
{{{},()},} is non empty set
{[{},()]} is non empty Relation-like Function-like set
rng op1 is non empty Element of bool 1
{()} is non empty set
is non empty Relation-like set
X is set
f is set

[: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

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

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

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

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

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

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

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

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

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

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 \ () is Element of bool f
bool f is non empty set
() \/ (f \ ()) 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

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

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 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