:: BVFUNC_2 semantic presentation

K120() is Element of bool K116()
K116() is set
bool K116() is non empty set
K115() is set
bool K115() is non empty set
bool K120() is non empty set
BOOLEAN is non empty set
{} is empty V55() set
the empty V55() set is empty V55() set
FALSE is V39() boolean Element of BOOLEAN
K121() is empty V55() Element of K120()
TRUE is V39() boolean Element of BOOLEAN
1 is non empty set
FALSE is V39() boolean set
TRUE is V39() boolean set
Y is set
PARTITIONS Y is non empty set
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
bool (bool Y) is non empty Element of bool (bool (bool Y))
G is set
G is set
Y is set
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
G is non empty partition-membered Element of bool (bool (bool Y))
u is Element of G
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
bool Y is non empty set
bool (bool Y) is non empty set
G is Element of bool (PARTITIONS Y)
u is Element of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
[:(Y),(bool Y):] is non empty set
bool [:(Y),(bool Y):] is non empty set
a is Relation-like (Y) -defined bool Y -valued Function-like Element of bool [:(Y),(bool Y):]
dom a is Element of bool (Y)
bool (Y) is non empty set
PA is set
PA is set
a . PA is set
z is non empty with_non-empty_elements a_partition of Y
a /. z is Element of bool Y
a . z is set
EqClass (u,z) is Element of z
PA is set
rng a is Element of bool (bool Y)
z is non empty with_non-empty_elements (Y,(Y))
a . z is set
a /. z is Element of bool Y
EqClass (u,z) is Element of z
z is set
x1 is set
a . x1 is set
PA is Element of bool (bool Y)
Intersect PA is Element of bool Y
meet (rng a) is Element of bool Y
PA is Element of bool (bool Y)
Intersect PA is Element of bool Y
Y is non empty set
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
bool (Y) is non empty set
G is Element of bool (Y)
u is set
a is Element of bool Y
PA is Relation-like Function-like set
dom PA is set
rng PA is set
z is Element of bool (bool Y)
Intersect z is Element of bool Y
x1 is Element of bool Y
x2 is Relation-like Function-like set
dom x2 is set
rng x2 is set
x2 is Element of bool (bool Y)
Intersect x2 is Element of bool Y
x is set
meet (rng x2) is set
meet (rng PA) is set
ad is set
PA . ad is set
x2 . ad is set
g is non empty with_non-empty_elements a_partition of Y
PA . g is set
x2 . g is set
union u is set
a is set
PA is Element of Y
z is Element of bool Y
x1 is Relation-like Function-like set
dom x1 is set
rng x1 is set
x2 is Element of bool (bool Y)
Intersect x2 is Element of bool Y
a is set
PA is set
z is Relation-like Function-like set
dom z is set
rng z is set
x1 is Element of bool (bool Y)
Intersect x1 is Element of bool Y
a is set
a is Element of bool (bool Y)
PA is set
x1 is Relation-like Function-like set
dom x1 is set
rng x1 is set
x2 is Element of bool (bool Y)
z is set
Intersect x2 is Element of bool Y
u is non empty with_non-empty_elements a_partition of Y
a is non empty with_non-empty_elements a_partition of Y
PA is set
z is Relation-like Function-like set
dom z is set
rng z is set
x1 is Element of bool (bool Y)
Intersect x1 is Element of bool Y
z is Relation-like Function-like set
dom z is set
rng z is set
x1 is Element of bool (bool Y)
Intersect x1 is Element of bool Y
Y is non empty set
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
bool (Y) is non empty set
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
bool Y is non empty set
G is Element of bool (PARTITIONS Y)
u is Element of Y
bool (bool Y) is non empty set
{ b₁ where b₁ is Element of bool Y : S₁[b₁] } is set
a is Element of bool (bool Y)
z is set
x1 is non empty with_non-empty_elements a_partition of Y
union x1 is Element of bool Y
PA is Element of bool (bool Y)
Intersect PA is Element of bool Y
x2 is non empty with_non-empty_elements a_partition of Y
x2 is set
x2 is set
x2 is set
x2 is set
union x2 is set
x is set
meet PA is Element of bool Y
x is Element of bool Y
x ` is Element of bool Y
Y \ x is Element of bool Y
ad is non empty with_non-empty_elements a_partition of Y
ad is set
meet PA is Element of bool Y
x /\ x is Element of bool Y
ad is set
x /\ (x `) is Element of bool Y
x /\ (Intersect PA) is Element of bool Y
x2 is set
x2 is Element of bool Y
meet PA is Element of bool Y
x2 is non empty with_non-empty_elements a_partition of Y
x2 is set
x is Element of bool Y
Y is non empty set
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
bool (Y) is non empty set
G is Element of bool (Y)
SmallestPartition Y is non empty with_non-empty_elements a_partition of Y
u is set
union u is set
a is set
PA is set
a is set
PA is non empty with_non-empty_elements a_partition of Y
union PA is Element of bool Y
z is set
x1 is set
x2 is set
union x2 is set
z is set
x1 is Element of Y
x2 is Element of bool Y
z is set
x1 is set
z is Element of bool Y
x1 is set
union x1 is set
x2 is set
x2 is Element of bool Y
z /\ x2 is Element of bool Y
x is non empty with_non-empty_elements a_partition of Y
x is set
x is set
z is set
z is Element of bool (bool Y)
x1 is set
x2 is set
u is non empty with_non-empty_elements a_partition of Y
a is non empty with_non-empty_elements a_partition of Y
PA is set
z is set
PA is set
z is set
x1 is set
x2 is set
Y is non empty set
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
bool (Y) is non empty set
G is Element of bool (Y)
(Y,G) is non empty with_non-empty_elements a_partition of Y
u is non empty with_non-empty_elements a_partition of Y
a is set
PA is Relation-like Function-like set
dom PA is set
rng PA is set
z is Element of bool (bool Y)
Intersect z is Element of bool Y
PA . u is set
meet z is Element of bool Y
Y is non empty set
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
bool (Y) is non empty set
G is Element of bool (Y)
(Y,G) is non empty with_non-empty_elements a_partition of Y
u is non empty with_non-empty_elements a_partition of Y
a is set
the Element of a is Element of a
union (Y,G) is Element of bool Y
z is set
x1 is set
union x1 is set
x2 is set
a /\ x2 is set
Y is non empty set
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
bool (Y) is non empty set
Y is non empty set
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
bool (Y) is non empty set
Y is non empty set
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
bool (Y) is non empty set
Y is non empty set
G is non empty with_non-empty_elements a_partition of Y
{G} is non empty set
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
bool (Y) is non empty set
Y is non empty set
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
bool (Y) is non empty set
u is Element of bool (Y)
G is non empty with_non-empty_elements a_partition of Y
(Y,G) is non empty Element of bool (Y)
u \ (Y,G) is Element of bool (Y)
(Y,(u \ (Y,G))) is non empty with_non-empty_elements a_partition of Y
Y is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
bool (Y) is non empty set
Y is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
bool (Y) is non empty set
G is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is non empty with_non-empty_elements a_partition of Y
u is Element of bool (Y)
(Y,a,u) is non empty with_non-empty_elements a_partition of Y
(Y,a) is non empty Element of bool (Y)
u \ (Y,a) is Element of bool (Y)
(Y,(u \ (Y,a))) is non empty with_non-empty_elements a_partition of Y
B_INF (G,(Y,a,u)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
bool (Y) is non empty set
G is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is non empty with_non-empty_elements a_partition of Y
u is Element of bool (Y)
(Y,a,u) is non empty with_non-empty_elements a_partition of Y
(Y,a) is non empty Element of bool (Y)
u \ (Y,a) is Element of bool (Y)
(Y,(u \ (Y,a))) is non empty with_non-empty_elements a_partition of Y
B_SUP (G,(Y,a,u)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is non empty with_non-empty_elements a_partition of Y
(Y,u,G,a) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,a) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,a) is Element of bool (Y)
(Y,(G \ (Y,a))) is non empty with_non-empty_elements a_partition of Y
B_INF (u,(Y,a,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is set
z is set
x1 is set
(Y,u,G,a) . z is V39() boolean set
(Y,u,G,a) . x1 is V39() boolean set
x2 is Element of Y
EqClass (x2,(Y,a,G)) is Element of (Y,a,G)
x2 is Element of Y
EqClass (x2,(Y,a,G)) is Element of (Y,a,G)
(Y,u,G,a) . x2 is V39() boolean Element of BOOLEAN
x is Element of Y
u . x is V39() boolean Element of BOOLEAN
x is Element of Y
u . x is V39() boolean Element of BOOLEAN
(Y,u,G,a) . x2 is V39() boolean Element of BOOLEAN
x is Element of Y
u . x is V39() boolean Element of BOOLEAN
ad is Element of Y
u . ad is V39() boolean Element of BOOLEAN
x is Element of Y
u . x is V39() boolean Element of BOOLEAN
ad is Element of Y
u . ad is V39() boolean Element of BOOLEAN
x is Element of Y
u . x is V39() boolean Element of BOOLEAN
ad is Element of Y
u . ad is V39() boolean Element of BOOLEAN
g is Element of Y
u . g is V39() boolean Element of BOOLEAN
c₁₃ is Element of Y
u . c₁₃ is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is non empty with_non-empty_elements a_partition of Y
(Y,u,G,a) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,a) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,a) is Element of bool (Y)
(Y,(G \ (Y,a))) is non empty with_non-empty_elements a_partition of Y
B_SUP (u,(Y,a,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is set
z is set
x1 is set
(Y,u,G,a) . z is V39() boolean set
(Y,u,G,a) . x1 is V39() boolean set
x2 is Element of Y
EqClass (x2,(Y,a,G)) is Element of (Y,a,G)
x2 is Element of Y
EqClass (x2,(Y,a,G)) is Element of (Y,a,G)
(B_SUP (u,(Y,a,G))) . x2 is V39() boolean Element of BOOLEAN
x is Element of Y
u . x is V39() boolean Element of BOOLEAN
ad is Element of Y
u . ad is V39() boolean Element of BOOLEAN
x is Element of Y
u . x is V39() boolean Element of BOOLEAN
ad is Element of Y
u . ad is V39() boolean Element of BOOLEAN
x is Element of Y
u . x is V39() boolean Element of BOOLEAN
x is Element of Y
u . x is V39() boolean Element of BOOLEAN
(B_SUP (u,(Y,a,G))) . x2 is V39() boolean Element of BOOLEAN
x is Element of Y
u . x is V39() boolean Element of BOOLEAN
ad is Element of Y
u . ad is V39() boolean Element of BOOLEAN
g is Element of Y
u . g is V39() boolean Element of BOOLEAN
c₁₃ is Element of Y
u . c₁₃ is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
I_el Y is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
a is non empty with_non-empty_elements a_partition of Y
(Y,(I_el Y),G,a) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,a) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,a) is Element of bool (Y)
(Y,(G \ (Y,a))) is non empty with_non-empty_elements a_partition of Y
B_INF ((I_el Y),(Y,a,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is Element of Y
(Y,(I_el Y),G,a) . PA is V39() boolean Element of BOOLEAN
EqClass (PA,(Y,a,G)) is Element of (Y,a,G)
z is Element of Y
(I_el Y) . z is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
I_el Y is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
a is non empty with_non-empty_elements a_partition of Y
(Y,(I_el Y),G,a) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,a) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,a) is Element of bool (Y)
(Y,(G \ (Y,a))) is non empty with_non-empty_elements a_partition of Y
B_SUP ((I_el Y),(Y,a,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is Element of Y
(Y,(I_el Y),G,a) . PA is V39() boolean Element of BOOLEAN
EqClass (PA,(Y,a,G)) is Element of (Y,a,G)
(I_el Y) . PA is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
O_el Y is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
a is non empty with_non-empty_elements a_partition of Y
(Y,(O_el Y),G,a) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,a) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,a) is Element of bool (Y)
(Y,(G \ (Y,a))) is non empty with_non-empty_elements a_partition of Y
B_INF ((O_el Y),(Y,a,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is Element of Y
(Y,(O_el Y),G,a) . PA is V39() boolean Element of BOOLEAN
EqClass (PA,(Y,a,G)) is Element of (Y,a,G)
(O_el Y) . PA is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
O_el Y is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
a is non empty with_non-empty_elements a_partition of Y
(Y,(O_el Y),G,a) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,a) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,a) is Element of bool (Y)
(Y,(G \ (Y,a))) is non empty with_non-empty_elements a_partition of Y
B_SUP ((O_el Y),(Y,a,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is Element of Y
(Y,(O_el Y),G,a) . PA is V39() boolean Element of BOOLEAN
EqClass (PA,(Y,a,G)) is Element of (Y,a,G)
z is Element of Y
(O_el Y) . z is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is non empty with_non-empty_elements a_partition of Y
(Y,u,G,a) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,a) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,a) is Element of bool (Y)
(Y,(G \ (Y,a))) is non empty with_non-empty_elements a_partition of Y
B_INF (u,(Y,a,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is Element of Y
(Y,u,G,a) . PA is V39() boolean Element of BOOLEAN
u . PA is V39() boolean Element of BOOLEAN
EqClass (PA,(Y,a,G)) is Element of (Y,a,G)
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is non empty with_non-empty_elements a_partition of Y
(Y,u,G,a) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,a) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,a) is Element of bool (Y)
(Y,(G \ (Y,a))) is non empty with_non-empty_elements a_partition of Y
B_SUP (u,(Y,a,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is Element of Y
u . PA is V39() boolean Element of BOOLEAN
(Y,u,G,a) . PA is V39() boolean Element of BOOLEAN
EqClass (PA,(Y,a,G)) is Element of (Y,a,G)
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'or' a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is non empty with_non-empty_elements a_partition of Y
(Y,u,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_INF (u,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_INF (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,u,G,PA) 'or' (Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,(u 'or' a),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_INF ((u 'or' a),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
((Y,u,G,PA) 'or' (Y,a,G,PA)) . z is V39() boolean Element of BOOLEAN
(Y,(u 'or' a),G,PA) . z is V39() boolean Element of BOOLEAN
(Y,u,G,PA) . z is V39() boolean Element of BOOLEAN
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
((Y,u,G,PA) . z) 'or' ((Y,a,G,PA) . z) is V39() boolean set
'not' ((Y,u,G,PA) . z) is V39() boolean set
'not' ((Y,a,G,PA) . z) is V39() boolean set
('not' ((Y,u,G,PA) . z)) '&' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (('not' ((Y,u,G,PA) . z)) '&' ('not' ((Y,a,G,PA) . z))) is V39() boolean set
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
(u 'or' a) . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
a . x1 is V39() boolean Element of BOOLEAN
(u . x1) 'or' (a . x1) is V39() boolean set
'not' (u . x1) is V39() boolean set
'not' (a . x1) is V39() boolean set
('not' (u . x1)) '&' ('not' (a . x1)) is V39() boolean set
'not' (('not' (u . x1)) '&' ('not' (a . x1))) is V39() boolean set
TRUE 'or' (a . x1) is V39() boolean set
'not' TRUE is V39() boolean set
('not' TRUE) '&' ('not' (a . x1)) is V39() boolean set
'not' (('not' TRUE) '&' ('not' (a . x1))) is V39() boolean set
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
(u 'or' a) . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
a . x1 is V39() boolean Element of BOOLEAN
(u . x1) 'or' (a . x1) is V39() boolean set
'not' (u . x1) is V39() boolean set
'not' (a . x1) is V39() boolean set
('not' (u . x1)) '&' ('not' (a . x1)) is V39() boolean set
'not' (('not' (u . x1)) '&' ('not' (a . x1))) is V39() boolean set
(u . x1) 'or' TRUE is V39() boolean set
'not' TRUE is V39() boolean set
('not' (u . x1)) '&' ('not' TRUE) is V39() boolean set
'not' (('not' (u . x1)) '&' ('not' TRUE)) is V39() boolean set
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'imp' a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is non empty with_non-empty_elements a_partition of Y
(Y,(u 'imp' a),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_INF ((u 'imp' a),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,u,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_INF (u,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_INF (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,u,G,PA) 'imp' (Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
(Y,(u 'imp' a),G,PA) . z is V39() boolean Element of BOOLEAN
((Y,u,G,PA) 'imp' (Y,a,G,PA)) . z is V39() boolean Element of BOOLEAN
(Y,u,G,PA) . z is V39() boolean Element of BOOLEAN
'not' ((Y,u,G,PA) . z) is V39() boolean Element of BOOLEAN
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
('not' ((Y,u,G,PA) . z)) 'or' ((Y,a,G,PA) . z) is V39() boolean set
'not' ('not' ((Y,u,G,PA) . z)) is V39() boolean set
'not' ((Y,a,G,PA) . z) is V39() boolean set
('not' ('not' ((Y,u,G,PA) . z))) '&' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (('not' ('not' ((Y,u,G,PA) . z))) '&' ('not' ((Y,a,G,PA) . z))) is V39() boolean set
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
(B_INF (a,(Y,PA,G))) . z is V39() boolean Element of BOOLEAN
('not' ((Y,u,G,PA) . z)) 'or' TRUE is V39() boolean set
'not' TRUE is V39() boolean set
('not' ('not' ((Y,u,G,PA) . z))) '&' ('not' TRUE) is V39() boolean set
'not' (('not' ('not' ((Y,u,G,PA) . z))) '&' ('not' TRUE)) is V39() boolean set
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
(u 'imp' a) . x1 is V39() boolean Element of BOOLEAN
'not' (u . x1) is V39() boolean Element of BOOLEAN
('not' (u . x1)) 'or' (a . x1) is V39() boolean set
'not' ('not' (u . x1)) is V39() boolean set
'not' (a . x1) is V39() boolean set
('not' ('not' (u . x1))) '&' ('not' (a . x1)) is V39() boolean set
'not' (('not' ('not' (u . x1))) '&' ('not' (a . x1))) is V39() boolean set
'not' TRUE is V39() boolean Element of BOOLEAN
('not' TRUE) 'or' FALSE is V39() boolean set
'not' ('not' TRUE) is V39() boolean set
'not' FALSE is V39() boolean set
('not' ('not' TRUE)) '&' ('not' FALSE) is V39() boolean set
'not' (('not' ('not' TRUE)) '&' ('not' FALSE)) is V39() boolean set
FALSE 'or' FALSE is V39() boolean set
('not' FALSE) '&' ('not' FALSE) is V39() boolean set
'not' (('not' FALSE) '&' ('not' FALSE)) is V39() boolean set
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
('not' ((Y,u,G,PA) . z)) 'or' TRUE is V39() boolean set
'not' TRUE is V39() boolean set
('not' ('not' ((Y,u,G,PA) . z))) '&' ('not' TRUE) is V39() boolean set
'not' (('not' ('not' ((Y,u,G,PA) . z))) '&' ('not' TRUE)) is V39() boolean set
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
TRUE 'or' ((Y,a,G,PA) . z) is V39() boolean set
'not' TRUE is V39() boolean set
('not' TRUE) '&' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (('not' TRUE) '&' ('not' ((Y,a,G,PA) . z))) is V39() boolean set
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
x2 is Element of Y
u . x2 is V39() boolean Element of BOOLEAN
x is Element of Y
a . x is V39() boolean Element of BOOLEAN
Y is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
bool (Y) is non empty set
G is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G '&' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is Element of bool (Y)
PA is non empty with_non-empty_elements a_partition of Y
(Y,(G '&' u),a,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,a) is non empty with_non-empty_elements a_partition of Y
(Y,PA) is non empty Element of bool (Y)
a \ (Y,PA) is Element of bool (Y)
(Y,(a \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_SUP ((G '&' u),(Y,PA,a)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,G,a,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_SUP (G,(Y,PA,a)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,u,a,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_SUP (u,(Y,PA,a)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,G,a,PA) '&' (Y,u,a,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
(Y,(G '&' u),a,PA) . z is V39() boolean Element of BOOLEAN
((Y,G,a,PA) '&' (Y,u,a,PA)) . z is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,a)) is Element of (Y,PA,a)
x1 is Element of Y
(G '&' u) . x1 is V39() boolean Element of BOOLEAN
G . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
(G . x1) '&' (u . x1) is V39() boolean Element of BOOLEAN
(Y,G,a,PA) . z is V39() boolean Element of BOOLEAN
(Y,u,a,PA) . z is V39() boolean Element of BOOLEAN
((Y,G,a,PA) . z) '&' ((Y,u,a,PA) . z) is V39() boolean Element of BOOLEAN
TRUE '&' TRUE is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'xor' a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is non empty with_non-empty_elements a_partition of Y
(Y,u,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_SUP (u,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_SUP (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,u,G,PA) 'xor' (Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,(u 'xor' a),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_SUP ((u 'xor' a),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
((Y,u,G,PA) 'xor' (Y,a,G,PA)) . z is V39() boolean Element of BOOLEAN
(Y,(u 'xor' a),G,PA) . z is V39() boolean Element of BOOLEAN
(Y,u,G,PA) . z is V39() boolean Element of BOOLEAN
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
((Y,u,G,PA) . z) 'xor' ((Y,a,G,PA) . z) is V39() boolean set
((Y,u,G,PA) . z) <=> ((Y,a,G,PA) . z) is V39() boolean set
'not' (((Y,u,G,PA) . z) 'xor' ((Y,a,G,PA) . z)) is V39() boolean set
((Y,u,G,PA) . z) => ((Y,a,G,PA) . z) is V39() boolean set
'not' ((Y,u,G,PA) . z) is V39() boolean set
('not' ((Y,u,G,PA) . z)) 'or' ((Y,a,G,PA) . z) is V39() boolean set
'not' ('not' ((Y,u,G,PA) . z)) is V39() boolean set
'not' ((Y,a,G,PA) . z) is V39() boolean set
('not' ('not' ((Y,u,G,PA) . z))) '&' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (('not' ('not' ((Y,u,G,PA) . z))) '&' ('not' ((Y,a,G,PA) . z))) is V39() boolean set
((Y,a,G,PA) . z) => ((Y,u,G,PA) . z) is V39() boolean set
('not' ((Y,a,G,PA) . z)) 'or' ((Y,u,G,PA) . z) is V39() boolean set
'not' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
('not' ('not' ((Y,a,G,PA) . z))) '&' ('not' ((Y,u,G,PA) . z)) is V39() boolean set
'not' (('not' ('not' ((Y,a,G,PA) . z))) '&' ('not' ((Y,u,G,PA) . z))) is V39() boolean set
(((Y,u,G,PA) . z) => ((Y,a,G,PA) . z)) '&' (((Y,a,G,PA) . z) => ((Y,u,G,PA) . z)) is V39() boolean set
'not' (((Y,u,G,PA) . z) <=> ((Y,a,G,PA) . z)) is V39() boolean set
'not' ((Y,u,G,PA) . z) is V39() boolean Element of BOOLEAN
('not' ((Y,u,G,PA) . z)) '&' ((Y,a,G,PA) . z) is V39() boolean Element of BOOLEAN
'not' ((Y,a,G,PA) . z) is V39() boolean Element of BOOLEAN
((Y,u,G,PA) . z) '&' ('not' ((Y,a,G,PA) . z)) is V39() boolean Element of BOOLEAN
(('not' ((Y,u,G,PA) . z)) '&' ((Y,a,G,PA) . z)) 'or' (((Y,u,G,PA) . z) '&' ('not' ((Y,a,G,PA) . z))) is V39() boolean set
'not' (('not' ((Y,u,G,PA) . z)) '&' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (((Y,u,G,PA) . z) '&' ('not' ((Y,a,G,PA) . z))) is V39() boolean set
('not' (('not' ((Y,u,G,PA) . z)) '&' ((Y,a,G,PA) . z))) '&' ('not' (((Y,u,G,PA) . z) '&' ('not' ((Y,a,G,PA) . z)))) is V39() boolean set
'not' (('not' (('not' ((Y,u,G,PA) . z)) '&' ((Y,a,G,PA) . z))) '&' ('not' (((Y,u,G,PA) . z) '&' ('not' ((Y,a,G,PA) . z))))) is V39() boolean set
'not' FALSE is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
(u 'xor' a) . x1 is V39() boolean Element of BOOLEAN
(u . x1) 'xor' (a . x1) is V39() boolean set
(u . x1) <=> (a . x1) is V39() boolean set
'not' ((u . x1) 'xor' (a . x1)) is V39() boolean set
(u . x1) => (a . x1) is V39() boolean set
'not' (u . x1) is V39() boolean set
('not' (u . x1)) 'or' (a . x1) is V39() boolean set
'not' ('not' (u . x1)) is V39() boolean set
'not' (a . x1) is V39() boolean set
('not' ('not' (u . x1))) '&' ('not' (a . x1)) is V39() boolean set
'not' (('not' ('not' (u . x1))) '&' ('not' (a . x1))) is V39() boolean set
(a . x1) => (u . x1) is V39() boolean set
('not' (a . x1)) 'or' (u . x1) is V39() boolean set
'not' ('not' (a . x1)) is V39() boolean set
('not' ('not' (a . x1))) '&' ('not' (u . x1)) is V39() boolean set
'not' (('not' ('not' (a . x1))) '&' ('not' (u . x1))) is V39() boolean set
((u . x1) => (a . x1)) '&' ((a . x1) => (u . x1)) is V39() boolean set
'not' ((u . x1) <=> (a . x1)) is V39() boolean set
TRUE 'or' FALSE is V39() boolean set
'not' TRUE is V39() boolean set
'not' FALSE is V39() boolean set
('not' TRUE) '&' ('not' FALSE) is V39() boolean set
'not' (('not' TRUE) '&' ('not' FALSE)) is V39() boolean set
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
a . x1 is V39() boolean Element of BOOLEAN
(u 'xor' a) . x1 is V39() boolean Element of BOOLEAN
(u . x1) 'xor' (a . x1) is V39() boolean set
(u . x1) <=> (a . x1) is V39() boolean set
'not' ((u . x1) 'xor' (a . x1)) is V39() boolean set
(u . x1) => (a . x1) is V39() boolean set
'not' (u . x1) is V39() boolean set
('not' (u . x1)) 'or' (a . x1) is V39() boolean set
'not' ('not' (u . x1)) is V39() boolean set
'not' (a . x1) is V39() boolean set
('not' ('not' (u . x1))) '&' ('not' (a . x1)) is V39() boolean set
'not' (('not' ('not' (u . x1))) '&' ('not' (a . x1))) is V39() boolean set
(a . x1) => (u . x1) is V39() boolean set
('not' (a . x1)) 'or' (u . x1) is V39() boolean set
'not' ('not' (a . x1)) is V39() boolean set
('not' ('not' (a . x1))) '&' ('not' (u . x1)) is V39() boolean set
'not' (('not' ('not' (a . x1))) '&' ('not' (u . x1))) is V39() boolean set
((u . x1) => (a . x1)) '&' ((a . x1) => (u . x1)) is V39() boolean set
'not' ((u . x1) <=> (a . x1)) is V39() boolean set
FALSE 'or' TRUE is V39() boolean set
'not' FALSE is V39() boolean set
'not' TRUE is V39() boolean set
('not' FALSE) '&' ('not' TRUE) is V39() boolean set
'not' (('not' FALSE) '&' ('not' TRUE)) is V39() boolean set
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'imp' a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is non empty with_non-empty_elements a_partition of Y
(Y,u,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_SUP (u,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_SUP (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,u,G,PA) 'imp' (Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,(u 'imp' a),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_SUP ((u 'imp' a),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
((Y,u,G,PA) 'imp' (Y,a,G,PA)) . z is V39() boolean Element of BOOLEAN
(Y,(u 'imp' a),G,PA) . z is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
(Y,u,G,PA) . z is V39() boolean Element of BOOLEAN
'not' ((Y,u,G,PA) . z) is V39() boolean Element of BOOLEAN
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
('not' ((Y,u,G,PA) . z)) 'or' ((Y,a,G,PA) . z) is V39() boolean set
'not' ('not' ((Y,u,G,PA) . z)) is V39() boolean set
'not' ((Y,a,G,PA) . z) is V39() boolean set
('not' ('not' ((Y,u,G,PA) . z))) '&' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (('not' ('not' ((Y,u,G,PA) . z))) '&' ('not' ((Y,a,G,PA) . z))) is V39() boolean set
u . z is V39() boolean Element of BOOLEAN
(u 'imp' a) . z is V39() boolean Element of BOOLEAN
'not' (u . z) is V39() boolean Element of BOOLEAN
a . z is V39() boolean Element of BOOLEAN
('not' (u . z)) 'or' (a . z) is V39() boolean set
'not' ('not' (u . z)) is V39() boolean set
'not' (a . z) is V39() boolean set
('not' ('not' (u . z))) '&' ('not' (a . z)) is V39() boolean set
'not' (('not' ('not' (u . z))) '&' ('not' (a . z))) is V39() boolean set
TRUE 'or' (a . z) is V39() boolean set
'not' TRUE is V39() boolean set
('not' TRUE) '&' ('not' (a . z)) is V39() boolean set
'not' (('not' TRUE) '&' ('not' (a . z))) is V39() boolean set
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
(u 'imp' a) . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
'not' (u . x1) is V39() boolean Element of BOOLEAN
('not' (u . x1)) 'or' (a . x1) is V39() boolean set
'not' ('not' (u . x1)) is V39() boolean set
'not' (a . x1) is V39() boolean set
('not' ('not' (u . x1))) '&' ('not' (a . x1)) is V39() boolean set
'not' (('not' ('not' (u . x1))) '&' ('not' (a . x1))) is V39() boolean set
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is non empty with_non-empty_elements a_partition of Y
(Y,u,G,a) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,a) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,a) is Element of bool (Y)
(Y,(G \ (Y,a))) is non empty with_non-empty_elements a_partition of Y
B_INF (u,(Y,a,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Y,u,G,a) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,('not' u),G,a) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_SUP (('not' u),(Y,a,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is Element of Y
('not' (Y,u,G,a)) . PA is V39() boolean set
(Y,('not' u),G,a) . PA is V39() boolean set
EqClass (PA,(Y,a,G)) is Element of (Y,a,G)
z is Element of Y
('not' u) . z is V39() boolean Element of BOOLEAN
z is Element of Y
('not' u) . z is V39() boolean Element of BOOLEAN
u . z is V39() boolean Element of BOOLEAN
'not' (u . z) is V39() boolean Element of BOOLEAN
x1 is Element of Y
('not' u) . x1 is V39() boolean Element of BOOLEAN
EqClass (PA,(Y,a,G)) is Element of (Y,a,G)
(B_INF (u,(Y,a,G))) . PA is V39() boolean Element of BOOLEAN
'not' (B_INF (u,(Y,a,G))) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
('not' (B_INF (u,(Y,a,G)))) . PA is V39() boolean Element of BOOLEAN
'not' TRUE is V39() boolean Element of BOOLEAN
(B_SUP (('not' u),(Y,a,G))) . PA is V39() boolean Element of BOOLEAN
EqClass (PA,(Y,a,G)) is Element of (Y,a,G)
(B_INF (u,(Y,a,G))) . PA is V39() boolean Element of BOOLEAN
z is Element of Y
u . z is V39() boolean Element of BOOLEAN
x1 is Element of Y
('not' u) . x1 is V39() boolean Element of BOOLEAN
'not' (B_INF (u,(Y,a,G))) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
('not' (B_INF (u,(Y,a,G)))) . PA is V39() boolean Element of BOOLEAN
'not' FALSE is V39() boolean Element of BOOLEAN
(B_SUP (('not' u),(Y,a,G))) . PA is V39() boolean Element of BOOLEAN
z is Element of Y
u . z is V39() boolean Element of BOOLEAN
x1 is Element of Y
('not' u) . x1 is V39() boolean Element of BOOLEAN
EqClass (PA,(Y,a,G)) is Element of (Y,a,G)
z is Element of Y
u . z is V39() boolean Element of BOOLEAN
z is Element of Y
u . z is V39() boolean Element of BOOLEAN
('not' u) . z is V39() boolean Element of BOOLEAN
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
'not' (u . z) is V39() boolean Element of BOOLEAN
EqClass (PA,(Y,a,G)) is Element of (Y,a,G)
z is Element of Y
u . z is V39() boolean Element of BOOLEAN
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
('not' u) . x2 is V39() boolean Element of BOOLEAN
x2 is Element of Y
('not' u) . x2 is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is non empty with_non-empty_elements a_partition of Y
(Y,u,G,a) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,a) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,a) is Element of bool (Y)
(Y,(G \ (Y,a))) is non empty with_non-empty_elements a_partition of Y
B_SUP (u,(Y,a,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Y,u,G,a) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,('not' u),G,a) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_INF (('not' u),(Y,a,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is Element of Y
('not' (Y,u,G,a)) . PA is V39() boolean set
(Y,('not' u),G,a) . PA is V39() boolean set
EqClass (PA,(Y,a,G)) is Element of (Y,a,G)
z is Element of Y
u . z is V39() boolean Element of BOOLEAN
z is Element of Y
u . z is V39() boolean Element of BOOLEAN
('not' u) . z is V39() boolean Element of BOOLEAN
'not' TRUE is V39() boolean Element of BOOLEAN
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
EqClass (PA,(Y,a,G)) is Element of (Y,a,G)
(B_SUP (u,(Y,a,G))) . PA is V39() boolean Element of BOOLEAN
'not' ((B_SUP (u,(Y,a,G))) . PA) is V39() boolean Element of BOOLEAN
'not' (B_SUP (u,(Y,a,G))) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
('not' (B_SUP (u,(Y,a,G)))) . PA is V39() boolean Element of BOOLEAN
EqClass (PA,(Y,a,G)) is Element of (Y,a,G)
(B_SUP (u,(Y,a,G))) . PA is V39() boolean Element of BOOLEAN
z is Element of Y
('not' u) . z is V39() boolean Element of BOOLEAN
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
'not' (B_SUP (u,(Y,a,G))) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
('not' (B_SUP (u,(Y,a,G)))) . PA is V39() boolean Element of BOOLEAN
'not' TRUE is V39() boolean Element of BOOLEAN
(B_INF (('not' u),(Y,a,G))) . PA is V39() boolean Element of BOOLEAN
z is Element of Y
('not' u) . z is V39() boolean Element of BOOLEAN
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
EqClass (PA,(Y,a,G)) is Element of (Y,a,G)
z is Element of Y
('not' u) . z is V39() boolean Element of BOOLEAN
z is Element of Y
('not' u) . z is V39() boolean Element of BOOLEAN
u . z is V39() boolean Element of BOOLEAN
'not' (u . z) is V39() boolean Element of BOOLEAN
x1 is Element of Y
('not' u) . x1 is V39() boolean Element of BOOLEAN
EqClass (PA,(Y,a,G)) is Element of (Y,a,G)
z is Element of Y
('not' u) . z is V39() boolean Element of BOOLEAN
x1 is Element of Y
('not' u) . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
u . x2 is V39() boolean Element of BOOLEAN
x2 is Element of Y
u . x2 is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'imp' a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is non empty with_non-empty_elements a_partition of Y
(Y,(u 'imp' a),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_INF ((u 'imp' a),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_INF (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'imp' (Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
(u 'imp' (Y,a,G,PA)) . z is V39() boolean Element of BOOLEAN
(Y,(u 'imp' a),G,PA) . z is V39() boolean Element of BOOLEAN
u . z is V39() boolean Element of BOOLEAN
'not' (u . z) is V39() boolean Element of BOOLEAN
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
('not' (u . z)) 'or' ((Y,a,G,PA) . z) is V39() boolean set
'not' ('not' (u . z)) is V39() boolean set
'not' ((Y,a,G,PA) . z) is V39() boolean set
('not' ('not' (u . z))) '&' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (('not' ('not' (u . z))) '&' ('not' ((Y,a,G,PA) . z))) is V39() boolean set
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
(u 'imp' a) . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
'not' (u . x1) is V39() boolean Element of BOOLEAN
a . x1 is V39() boolean Element of BOOLEAN
('not' (u . x1)) 'or' (a . x1) is V39() boolean set
'not' ('not' (u . x1)) is V39() boolean set
'not' (a . x1) is V39() boolean set
('not' ('not' (u . x1))) '&' ('not' (a . x1)) is V39() boolean set
'not' (('not' ('not' (u . x1))) '&' ('not' (a . x1))) is V39() boolean set
('not' (u . x1)) 'or' TRUE is V39() boolean set
'not' TRUE is V39() boolean set
('not' ('not' (u . x1))) '&' ('not' TRUE) is V39() boolean set
'not' (('not' ('not' (u . x1))) '&' ('not' TRUE)) is V39() boolean set
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
(u 'imp' a) . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
'not' (u . x1) is V39() boolean Element of BOOLEAN
a . x1 is V39() boolean Element of BOOLEAN
('not' (u . x1)) 'or' (a . x1) is V39() boolean set
'not' ('not' (u . x1)) is V39() boolean set
'not' (a . x1) is V39() boolean set
('not' ('not' (u . x1))) '&' ('not' (a . x1)) is V39() boolean set
'not' (('not' ('not' (u . x1))) '&' ('not' (a . x1))) is V39() boolean set
z is Element of Y
(Y,(u 'imp' a),G,PA) . z is V39() boolean Element of BOOLEAN
(u 'imp' (Y,a,G,PA)) . z is V39() boolean Element of BOOLEAN
u . z is V39() boolean Element of BOOLEAN
'not' (u . z) is V39() boolean Element of BOOLEAN
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
('not' (u . z)) 'or' ((Y,a,G,PA) . z) is V39() boolean set
'not' ('not' (u . z)) is V39() boolean set
'not' ((Y,a,G,PA) . z) is V39() boolean set
('not' ('not' (u . z))) '&' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (('not' ('not' (u . z))) '&' ('not' ((Y,a,G,PA) . z))) is V39() boolean set
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
u . x2 is V39() boolean Element of BOOLEAN
'not' (u . x2) is V39() boolean Element of BOOLEAN
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
'not' (u . x1) is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
x2 is Element of Y
u . x2 is V39() boolean Element of BOOLEAN
'not' (u . x2) is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
u . x2 is V39() boolean Element of BOOLEAN
(u 'imp' a) . x2 is V39() boolean Element of BOOLEAN
'not' TRUE is V39() boolean Element of BOOLEAN
('not' TRUE) 'or' FALSE is V39() boolean set
'not' ('not' TRUE) is V39() boolean set
'not' FALSE is V39() boolean set
('not' ('not' TRUE)) '&' ('not' FALSE) is V39() boolean set
'not' (('not' ('not' TRUE)) '&' ('not' FALSE)) is V39() boolean set
FALSE 'or' FALSE is V39() boolean set
('not' FALSE) '&' ('not' FALSE) is V39() boolean set
'not' (('not' FALSE) '&' ('not' FALSE)) is V39() boolean set
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
u . x2 is V39() boolean Element of BOOLEAN
'not' (u . x2) is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a 'imp' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is non empty with_non-empty_elements a_partition of Y
(Y,(a 'imp' u),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_INF ((a 'imp' u),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_SUP (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) 'imp' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
((Y,a,G,PA) 'imp' u) . z is V39() boolean Element of BOOLEAN
(Y,(a 'imp' u),G,PA) . z is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
'not' ((Y,a,G,PA) . z) is V39() boolean Element of BOOLEAN
u . z is V39() boolean Element of BOOLEAN
('not' ((Y,a,G,PA) . z)) 'or' (u . z) is V39() boolean set
'not' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (u . z) is V39() boolean set
('not' ('not' ((Y,a,G,PA) . z))) '&' ('not' (u . z)) is V39() boolean set
'not' (('not' ('not' ((Y,a,G,PA) . z))) '&' ('not' (u . z))) is V39() boolean set
x1 is Element of Y
(a 'imp' u) . x1 is V39() boolean Element of BOOLEAN
a . x1 is V39() boolean Element of BOOLEAN
'not' (a . x1) is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
('not' (a . x1)) 'or' (u . x1) is V39() boolean set
'not' ('not' (a . x1)) is V39() boolean set
'not' (u . x1) is V39() boolean set
('not' ('not' (a . x1))) '&' ('not' (u . x1)) is V39() boolean set
'not' (('not' ('not' (a . x1))) '&' ('not' (u . x1))) is V39() boolean set
x1 is Element of Y
(a 'imp' u) . x1 is V39() boolean Element of BOOLEAN
a . x1 is V39() boolean Element of BOOLEAN
'not' (a . x1) is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
('not' (a . x1)) 'or' (u . x1) is V39() boolean set
'not' ('not' (a . x1)) is V39() boolean set
'not' (u . x1) is V39() boolean set
('not' ('not' (a . x1))) '&' ('not' (u . x1)) is V39() boolean set
'not' (('not' ('not' (a . x1))) '&' ('not' (u . x1))) is V39() boolean set
TRUE 'or' (u . x1) is V39() boolean set
'not' TRUE is V39() boolean set
('not' TRUE) '&' ('not' (u . x1)) is V39() boolean set
'not' (('not' TRUE) '&' ('not' (u . x1))) is V39() boolean set
z is Element of Y
(Y,(a 'imp' u),G,PA) . z is V39() boolean Element of BOOLEAN
((Y,a,G,PA) 'imp' u) . z is V39() boolean Element of BOOLEAN
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
'not' ((Y,a,G,PA) . z) is V39() boolean Element of BOOLEAN
u . z is V39() boolean Element of BOOLEAN
('not' ((Y,a,G,PA) . z)) 'or' (u . z) is V39() boolean set
'not' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (u . z) is V39() boolean set
('not' ('not' ((Y,a,G,PA) . z))) '&' ('not' (u . z)) is V39() boolean set
'not' (('not' ('not' ((Y,a,G,PA) . z))) '&' ('not' (u . z))) is V39() boolean set
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
('not' ((Y,a,G,PA) . z)) 'or' TRUE is V39() boolean set
'not' TRUE is V39() boolean set
('not' ('not' ((Y,a,G,PA) . z))) '&' ('not' TRUE) is V39() boolean set
'not' (('not' ('not' ((Y,a,G,PA) . z))) '&' ('not' TRUE)) is V39() boolean set
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
u . x2 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
u . x2 is V39() boolean Element of BOOLEAN
(a 'imp' u) . x2 is V39() boolean Element of BOOLEAN
'not' (a . x2) is V39() boolean Element of BOOLEAN
('not' (a . x2)) 'or' (u . x2) is V39() boolean set
'not' ('not' (a . x2)) is V39() boolean set
'not' (u . x2) is V39() boolean set
('not' ('not' (a . x2))) '&' ('not' (u . x2)) is V39() boolean set
'not' (('not' ('not' (a . x2))) '&' ('not' (u . x2))) is V39() boolean set
'not' TRUE is V39() boolean Element of BOOLEAN
('not' TRUE) 'or' FALSE is V39() boolean set
'not' ('not' TRUE) is V39() boolean set
'not' FALSE is V39() boolean set
('not' ('not' TRUE)) '&' ('not' FALSE) is V39() boolean set
'not' (('not' ('not' TRUE)) '&' ('not' FALSE)) is V39() boolean set
FALSE 'or' FALSE is V39() boolean set
('not' FALSE) '&' ('not' FALSE) is V39() boolean set
'not' (('not' FALSE) '&' ('not' FALSE)) is V39() boolean set
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
'not' FALSE is V39() boolean Element of BOOLEAN
('not' FALSE) 'or' (u . z) is V39() boolean set
'not' ('not' FALSE) is V39() boolean set
('not' ('not' FALSE)) '&' ('not' (u . z)) is V39() boolean set
'not' (('not' ('not' FALSE)) '&' ('not' (u . z))) is V39() boolean set
TRUE 'or' (u . z) is V39() boolean set
'not' TRUE is V39() boolean set
('not' TRUE) '&' ('not' (u . z)) is V39() boolean set
'not' (('not' TRUE) '&' ('not' (u . z))) is V39() boolean set
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'or' a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is non empty with_non-empty_elements a_partition of Y
(Y,(u 'or' a),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_INF ((u 'or' a),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_INF (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'or' (Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
(Y,(u 'or' a),G,PA) . z is V39() boolean set
(u 'or' (Y,a,G,PA)) . z is V39() boolean set
u 'or' (B_INF (a,(Y,PA,G))) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(u 'or' (B_INF (a,(Y,PA,G)))) . z is V39() boolean Element of BOOLEAN
u . z is V39() boolean Element of BOOLEAN
(B_INF (a,(Y,PA,G))) . z is V39() boolean Element of BOOLEAN
(u . z) 'or' ((B_INF (a,(Y,PA,G))) . z) is V39() boolean set
'not' (u . z) is V39() boolean set
'not' ((B_INF (a,(Y,PA,G))) . z) is V39() boolean set
('not' (u . z)) '&' ('not' ((B_INF (a,(Y,PA,G))) . z)) is V39() boolean set
'not' (('not' (u . z)) '&' ('not' ((B_INF (a,(Y,PA,G))) . z))) is V39() boolean set
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
(u 'or' a) . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
a . x1 is V39() boolean Element of BOOLEAN
(u . x1) 'or' (a . x1) is V39() boolean set
'not' (u . x1) is V39() boolean set
'not' (a . x1) is V39() boolean set
('not' (u . x1)) '&' ('not' (a . x1)) is V39() boolean set
'not' (('not' (u . x1)) '&' ('not' (a . x1))) is V39() boolean set
(u . x1) 'or' TRUE is V39() boolean set
'not' TRUE is V39() boolean set
('not' (u . x1)) '&' ('not' TRUE) is V39() boolean set
'not' (('not' (u . x1)) '&' ('not' TRUE)) is V39() boolean set
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
(u 'or' a) . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
a . x1 is V39() boolean Element of BOOLEAN
(u . x1) 'or' (a . x1) is V39() boolean set
'not' (u . x1) is V39() boolean set
'not' (a . x1) is V39() boolean set
('not' (u . x1)) '&' ('not' (a . x1)) is V39() boolean set
'not' (('not' (u . x1)) '&' ('not' (a . x1))) is V39() boolean set
TRUE 'or' (a . x1) is V39() boolean set
'not' TRUE is V39() boolean set
('not' TRUE) '&' ('not' (a . x1)) is V39() boolean set
'not' (('not' TRUE) '&' ('not' (a . x1))) is V39() boolean set
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
TRUE 'or' ((B_INF (a,(Y,PA,G))) . z) is V39() boolean set
'not' TRUE is V39() boolean set
('not' TRUE) '&' ('not' ((B_INF (a,(Y,PA,G))) . z)) is V39() boolean set
'not' (('not' TRUE) '&' ('not' ((B_INF (a,(Y,PA,G))) . z))) is V39() boolean set
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
u . x2 is V39() boolean Element of BOOLEAN
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
x2 is Element of Y
u . x2 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
u . x2 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
x is Element of Y
u . x is V39() boolean Element of BOOLEAN
(u 'or' a) . x2 is V39() boolean Element of BOOLEAN
FALSE 'or' FALSE is V39() boolean set
'not' FALSE is V39() boolean set
('not' FALSE) '&' ('not' FALSE) is V39() boolean set
'not' (('not' FALSE) '&' ('not' FALSE)) is V39() boolean set
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
u . x2 is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
PA is non empty with_non-empty_elements a_partition of Y
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a 'or' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,(a 'or' u),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_INF ((a 'or' u),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_INF (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) 'or' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a 'or' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is non empty with_non-empty_elements a_partition of Y
(Y,(a 'or' u),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_INF ((a 'or' u),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_SUP (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) 'or' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
(Y,(a 'or' u),G,PA) . z is V39() boolean Element of BOOLEAN
((Y,a,G,PA) 'or' u) . z is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
(a 'or' u) . x1 is V39() boolean Element of BOOLEAN
(a . x1) 'or' (u . x1) is V39() boolean set
'not' (a . x1) is V39() boolean set
'not' (u . x1) is V39() boolean set
('not' (a . x1)) '&' ('not' (u . x1)) is V39() boolean set
'not' (('not' (a . x1)) '&' ('not' (u . x1))) is V39() boolean set
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
u . z is V39() boolean Element of BOOLEAN
((Y,a,G,PA) . z) 'or' (u . z) is V39() boolean set
'not' ((Y,a,G,PA) . z) is V39() boolean set
'not' (u . z) is V39() boolean set
('not' ((Y,a,G,PA) . z)) '&' ('not' (u . z)) is V39() boolean set
'not' (('not' ((Y,a,G,PA) . z)) '&' ('not' (u . z))) is V39() boolean set
((Y,a,G,PA) . z) 'or' TRUE is V39() boolean set
'not' TRUE is V39() boolean set
('not' ((Y,a,G,PA) . z)) '&' ('not' TRUE) is V39() boolean set
'not' (('not' ((Y,a,G,PA) . z)) '&' ('not' TRUE)) is V39() boolean set
TRUE 'or' (u . z) is V39() boolean set
'not' TRUE is V39() boolean set
('not' TRUE) '&' ('not' (u . z)) is V39() boolean set
'not' (('not' TRUE) '&' ('not' (u . z))) is V39() boolean set
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
a . z is V39() boolean Element of BOOLEAN
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u '&' a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is non empty with_non-empty_elements a_partition of Y
(Y,(u '&' a),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_INF ((u '&' a),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_INF (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u '&' (Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
(Y,(u '&' a),G,PA) . z is V39() boolean Element of BOOLEAN
(u '&' (Y,a,G,PA)) . z is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
(u '&' a) . x1 is V39() boolean Element of BOOLEAN
a . x1 is V39() boolean Element of BOOLEAN
(u . x1) '&' (a . x1) is V39() boolean Element of BOOLEAN
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
(u '&' a) . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
(u . x1) '&' (a . x1) is V39() boolean Element of BOOLEAN
u . z is V39() boolean Element of BOOLEAN
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
(u . z) '&' ((Y,a,G,PA) . z) is V39() boolean Element of BOOLEAN
z is Element of Y
(u '&' (Y,a,G,PA)) . z is V39() boolean Element of BOOLEAN
(Y,(u '&' a),G,PA) . z is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
u . z is V39() boolean Element of BOOLEAN
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
(u . z) '&' ((Y,a,G,PA) . z) is V39() boolean Element of BOOLEAN
x1 is Element of Y
(u '&' a) . x1 is V39() boolean Element of BOOLEAN
a . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
TRUE '&' TRUE is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
PA is non empty with_non-empty_elements a_partition of Y
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a '&' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,(a '&' u),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_INF ((a '&' u),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_INF (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) '&' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u '&' a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is non empty with_non-empty_elements a_partition of Y
(Y,(u '&' a),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_INF ((u '&' a),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,u,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_SUP (u,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,u,G,PA) '&' a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
(Y,(u '&' a),G,PA) . z is V39() boolean Element of BOOLEAN
((Y,u,G,PA) '&' a) . z is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
a . x1 is V39() boolean Element of BOOLEAN
(u '&' a) . x1 is V39() boolean Element of BOOLEAN
(u . x1) '&' (a . x1) is V39() boolean Element of BOOLEAN
(Y,u,G,PA) . z is V39() boolean Element of BOOLEAN
a . z is V39() boolean Element of BOOLEAN
((Y,u,G,PA) . z) '&' (a . z) is V39() boolean Element of BOOLEAN
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
TRUE '&' TRUE is V39() boolean Element of BOOLEAN
u . z is V39() boolean Element of BOOLEAN
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'xor' a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is non empty with_non-empty_elements a_partition of Y
(Y,(u 'xor' a),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_INF ((u 'xor' a),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_INF (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'xor' (Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
(Y,(u 'xor' a),G,PA) . z is V39() boolean Element of BOOLEAN
(u 'xor' (Y,a,G,PA)) . z is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
'not' FALSE is V39() boolean Element of BOOLEAN
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
u . z is V39() boolean Element of BOOLEAN
((Y,a,G,PA) . z) 'xor' (u . z) is V39() boolean set
((Y,a,G,PA) . z) <=> (u . z) is V39() boolean set
'not' (((Y,a,G,PA) . z) 'xor' (u . z)) is V39() boolean set
((Y,a,G,PA) . z) => (u . z) is V39() boolean set
'not' ((Y,a,G,PA) . z) is V39() boolean set
('not' ((Y,a,G,PA) . z)) 'or' (u . z) is V39() boolean set
'not' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (u . z) is V39() boolean set
('not' ('not' ((Y,a,G,PA) . z))) '&' ('not' (u . z)) is V39() boolean set
'not' (('not' ('not' ((Y,a,G,PA) . z))) '&' ('not' (u . z))) is V39() boolean set
(u . z) => ((Y,a,G,PA) . z) is V39() boolean set
('not' (u . z)) 'or' ((Y,a,G,PA) . z) is V39() boolean set
'not' ('not' (u . z)) is V39() boolean set
('not' ('not' (u . z))) '&' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (('not' ('not' (u . z))) '&' ('not' ((Y,a,G,PA) . z))) is V39() boolean set
(((Y,a,G,PA) . z) => (u . z)) '&' ((u . z) => ((Y,a,G,PA) . z)) is V39() boolean set
'not' (((Y,a,G,PA) . z) <=> (u . z)) is V39() boolean set
a . z is V39() boolean Element of BOOLEAN
FALSE '&' TRUE is V39() boolean Element of BOOLEAN
(u 'xor' a) . z is V39() boolean Element of BOOLEAN
(a . z) 'xor' (u . z) is V39() boolean set
(a . z) <=> (u . z) is V39() boolean set
'not' ((a . z) 'xor' (u . z)) is V39() boolean set
(a . z) => (u . z) is V39() boolean set
'not' (a . z) is V39() boolean set
('not' (a . z)) 'or' (u . z) is V39() boolean set
'not' ('not' (a . z)) is V39() boolean set
('not' ('not' (a . z))) '&' ('not' (u . z)) is V39() boolean set
'not' (('not' ('not' (a . z))) '&' ('not' (u . z))) is V39() boolean set
(u . z) => (a . z) is V39() boolean set
('not' (u . z)) 'or' (a . z) is V39() boolean set
('not' ('not' (u . z))) '&' ('not' (a . z)) is V39() boolean set
'not' (('not' ('not' (u . z))) '&' ('not' (a . z))) is V39() boolean set
((a . z) => (u . z)) '&' ((u . z) => (a . z)) is V39() boolean set
'not' ((a . z) <=> (u . z)) is V39() boolean set
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
TRUE 'or' FALSE is V39() boolean set
'not' TRUE is V39() boolean set
'not' FALSE is V39() boolean set
('not' TRUE) '&' ('not' FALSE) is V39() boolean set
'not' (('not' TRUE) '&' ('not' FALSE)) is V39() boolean set
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
FALSE 'or' TRUE is V39() boolean set
'not' FALSE is V39() boolean set
'not' TRUE is V39() boolean set
('not' FALSE) '&' ('not' TRUE) is V39() boolean set
'not' (('not' FALSE) '&' ('not' TRUE)) is V39() boolean set
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
u . x2 is V39() boolean Element of BOOLEAN
(u 'xor' a) . x2 is V39() boolean Element of BOOLEAN
(a . x2) 'xor' (u . x2) is V39() boolean set
(a . x2) <=> (u . x2) is V39() boolean set
'not' ((a . x2) 'xor' (u . x2)) is V39() boolean set
(a . x2) => (u . x2) is V39() boolean set
'not' (a . x2) is V39() boolean set
('not' (a . x2)) 'or' (u . x2) is V39() boolean set
'not' ('not' (a . x2)) is V39() boolean set
'not' (u . x2) is V39() boolean set
('not' ('not' (a . x2))) '&' ('not' (u . x2)) is V39() boolean set
'not' (('not' ('not' (a . x2))) '&' ('not' (u . x2))) is V39() boolean set
(u . x2) => (a . x2) is V39() boolean set
('not' (u . x2)) 'or' (a . x2) is V39() boolean set
'not' ('not' (u . x2)) is V39() boolean set
('not' ('not' (u . x2))) '&' ('not' (a . x2)) is V39() boolean set
'not' (('not' ('not' (u . x2))) '&' ('not' (a . x2))) is V39() boolean set
((a . x2) => (u . x2)) '&' ((u . x2) => (a . x2)) is V39() boolean set
'not' ((a . x2) <=> (u . x2)) is V39() boolean set
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
x2 is Element of Y
u . x2 is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
PA is non empty with_non-empty_elements a_partition of Y
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a 'xor' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,(a 'xor' u),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_INF ((a 'xor' u),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_INF (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) 'xor' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'eqv' a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is non empty with_non-empty_elements a_partition of Y
(Y,(u 'eqv' a),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_INF ((u 'eqv' a),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_INF (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'eqv' (Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' FALSE is V39() boolean Element of BOOLEAN
z is Element of Y
(Y,(u 'eqv' a),G,PA) . z is V39() boolean Element of BOOLEAN
(u 'eqv' (Y,a,G,PA)) . z is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
u . z is V39() boolean Element of BOOLEAN
(u . z) 'xor' ((Y,a,G,PA) . z) is V39() boolean set
(u . z) <=> ((Y,a,G,PA) . z) is V39() boolean set
'not' ((u . z) 'xor' ((Y,a,G,PA) . z)) is V39() boolean set
(u . z) => ((Y,a,G,PA) . z) is V39() boolean set
'not' (u . z) is V39() boolean set
('not' (u . z)) 'or' ((Y,a,G,PA) . z) is V39() boolean set
'not' ('not' (u . z)) is V39() boolean set
'not' ((Y,a,G,PA) . z) is V39() boolean set
('not' ('not' (u . z))) '&' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (('not' ('not' (u . z))) '&' ('not' ((Y,a,G,PA) . z))) is V39() boolean set
((Y,a,G,PA) . z) => (u . z) is V39() boolean set
('not' ((Y,a,G,PA) . z)) 'or' (u . z) is V39() boolean set
'not' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
('not' ('not' ((Y,a,G,PA) . z))) '&' ('not' (u . z)) is V39() boolean set
'not' (('not' ('not' ((Y,a,G,PA) . z))) '&' ('not' (u . z))) is V39() boolean set
((u . z) => ((Y,a,G,PA) . z)) '&' (((Y,a,G,PA) . z) => (u . z)) is V39() boolean set
'not' ((u . z) <=> ((Y,a,G,PA) . z)) is V39() boolean set
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
(u 'eqv' a) . x1 is V39() boolean Element of BOOLEAN
(u . x1) 'xor' (a . x1) is V39() boolean set
(u . x1) <=> (a . x1) is V39() boolean set
'not' ((u . x1) 'xor' (a . x1)) is V39() boolean set
(u . x1) => (a . x1) is V39() boolean set
'not' (u . x1) is V39() boolean set
('not' (u . x1)) 'or' (a . x1) is V39() boolean set
'not' ('not' (u . x1)) is V39() boolean set
'not' (a . x1) is V39() boolean set
('not' ('not' (u . x1))) '&' ('not' (a . x1)) is V39() boolean set
'not' (('not' ('not' (u . x1))) '&' ('not' (a . x1))) is V39() boolean set
(a . x1) => (u . x1) is V39() boolean set
('not' (a . x1)) 'or' (u . x1) is V39() boolean set
'not' ('not' (a . x1)) is V39() boolean set
('not' ('not' (a . x1))) '&' ('not' (u . x1)) is V39() boolean set
'not' (('not' ('not' (a . x1))) '&' ('not' (u . x1))) is V39() boolean set
((u . x1) => (a . x1)) '&' ((a . x1) => (u . x1)) is V39() boolean set
'not' ((u . x1) <=> (a . x1)) is V39() boolean set
FALSE 'or' TRUE is V39() boolean set
'not' FALSE is V39() boolean set
'not' TRUE is V39() boolean set
('not' FALSE) '&' ('not' TRUE) is V39() boolean set
'not' (('not' FALSE) '&' ('not' TRUE)) is V39() boolean set
'not' (FALSE 'or' TRUE) is V39() boolean set
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
a . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
u . x2 is V39() boolean Element of BOOLEAN
(u 'eqv' a) . x1 is V39() boolean Element of BOOLEAN
(u . x1) 'xor' (a . x1) is V39() boolean set
(u . x1) <=> (a . x1) is V39() boolean set
'not' ((u . x1) 'xor' (a . x1)) is V39() boolean set
(u . x1) => (a . x1) is V39() boolean set
'not' (u . x1) is V39() boolean set
('not' (u . x1)) 'or' (a . x1) is V39() boolean set
'not' ('not' (u . x1)) is V39() boolean set
'not' (a . x1) is V39() boolean set
('not' ('not' (u . x1))) '&' ('not' (a . x1)) is V39() boolean set
'not' (('not' ('not' (u . x1))) '&' ('not' (a . x1))) is V39() boolean set
(a . x1) => (u . x1) is V39() boolean set
('not' (a . x1)) 'or' (u . x1) is V39() boolean set
'not' ('not' (a . x1)) is V39() boolean set
('not' ('not' (a . x1))) '&' ('not' (u . x1)) is V39() boolean set
'not' (('not' ('not' (a . x1))) '&' ('not' (u . x1))) is V39() boolean set
((u . x1) => (a . x1)) '&' ((a . x1) => (u . x1)) is V39() boolean set
'not' ((u . x1) <=> (a . x1)) is V39() boolean set
TRUE 'or' FALSE is V39() boolean set
'not' TRUE is V39() boolean set
'not' FALSE is V39() boolean set
('not' TRUE) '&' ('not' FALSE) is V39() boolean set
'not' (('not' TRUE) '&' ('not' FALSE)) is V39() boolean set
'not' (TRUE 'or' FALSE) is V39() boolean set
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
u . z is V39() boolean Element of BOOLEAN
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
x2 is Element of Y
u . x2 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
(u . z) 'xor' ((Y,a,G,PA) . z) is V39() boolean set
(u . z) <=> ((Y,a,G,PA) . z) is V39() boolean set
'not' ((u . z) 'xor' ((Y,a,G,PA) . z)) is V39() boolean set
(u . z) => ((Y,a,G,PA) . z) is V39() boolean set
'not' (u . z) is V39() boolean set
('not' (u . z)) 'or' ((Y,a,G,PA) . z) is V39() boolean set
'not' ('not' (u . z)) is V39() boolean set
'not' ((Y,a,G,PA) . z) is V39() boolean set
('not' ('not' (u . z))) '&' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (('not' ('not' (u . z))) '&' ('not' ((Y,a,G,PA) . z))) is V39() boolean set
((Y,a,G,PA) . z) => (u . z) is V39() boolean set
('not' ((Y,a,G,PA) . z)) 'or' (u . z) is V39() boolean set
'not' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
('not' ('not' ((Y,a,G,PA) . z))) '&' ('not' (u . z)) is V39() boolean set
'not' (('not' ('not' ((Y,a,G,PA) . z))) '&' ('not' (u . z))) is V39() boolean set
((u . z) => ((Y,a,G,PA) . z)) '&' (((Y,a,G,PA) . z) => (u . z)) is V39() boolean set
'not' ((u . z) <=> ((Y,a,G,PA) . z)) is V39() boolean set
x1 is Element of Y
u . x1 is V39() boolean Element of BOOLEAN
x2 is Element of Y
a . x2 is V39() boolean Element of BOOLEAN
x2 is Element of Y
u . x2 is V39() boolean Element of BOOLEAN
x is Element of Y
a . x is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
PA is non empty with_non-empty_elements a_partition of Y
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a 'eqv' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,(a 'eqv' u),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_INF ((a 'eqv' u),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_INF (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) 'eqv' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'or' a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is non empty with_non-empty_elements a_partition of Y
(Y,(u 'or' a),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_SUP ((u 'or' a),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_SUP (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'or' (Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
(Y,(u 'or' a),G,PA) . z is V39() boolean Element of BOOLEAN
(u 'or' (Y,a,G,PA)) . z is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
u . z is V39() boolean Element of BOOLEAN
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
(u . z) 'or' ((Y,a,G,PA) . z) is V39() boolean set
'not' (u . z) is V39() boolean set
'not' ((Y,a,G,PA) . z) is V39() boolean set
('not' (u . z)) '&' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (('not' (u . z)) '&' ('not' ((Y,a,G,PA) . z))) is V39() boolean set
x1 is Element of Y
(u 'or' a) . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
a . x1 is V39() boolean Element of BOOLEAN
(u . x1) 'or' (a . x1) is V39() boolean set
'not' (u . x1) is V39() boolean set
'not' (a . x1) is V39() boolean set
('not' (u . x1)) '&' ('not' (a . x1)) is V39() boolean set
'not' (('not' (u . x1)) '&' ('not' (a . x1))) is V39() boolean set
(u . z) 'or' TRUE is V39() boolean set
'not' TRUE is V39() boolean set
('not' (u . z)) '&' ('not' TRUE) is V39() boolean set
'not' (('not' (u . z)) '&' ('not' TRUE)) is V39() boolean set
z is Element of Y
(u 'or' (Y,a,G,PA)) . z is V39() boolean Element of BOOLEAN
(Y,(u 'or' a),G,PA) . z is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
u . z is V39() boolean Element of BOOLEAN
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
(u . z) 'or' ((Y,a,G,PA) . z) is V39() boolean set
'not' (u . z) is V39() boolean set
'not' ((Y,a,G,PA) . z) is V39() boolean set
('not' (u . z)) '&' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (('not' (u . z)) '&' ('not' ((Y,a,G,PA) . z))) is V39() boolean set
(u 'or' a) . z is V39() boolean Element of BOOLEAN
a . z is V39() boolean Element of BOOLEAN
TRUE 'or' (a . z) is V39() boolean set
'not' TRUE is V39() boolean set
'not' (a . z) is V39() boolean set
('not' TRUE) '&' ('not' (a . z)) is V39() boolean set
'not' (('not' TRUE) '&' ('not' (a . z))) is V39() boolean set
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
(u 'or' a) . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
(u . x1) 'or' (a . x1) is V39() boolean set
'not' (u . x1) is V39() boolean set
'not' (a . x1) is V39() boolean set
('not' (u . x1)) '&' ('not' (a . x1)) is V39() boolean set
'not' (('not' (u . x1)) '&' ('not' (a . x1))) is V39() boolean set
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
PA is non empty with_non-empty_elements a_partition of Y
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a 'or' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,(a 'or' u),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_SUP ((a 'or' u),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_SUP (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) 'or' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u '&' a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is non empty with_non-empty_elements a_partition of Y
(Y,(u '&' a),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_SUP ((u '&' a),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_SUP (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u '&' (Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
(Y,(u '&' a),G,PA) . z is V39() boolean Element of BOOLEAN
(u '&' (Y,a,G,PA)) . z is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
(u '&' a) . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
a . x1 is V39() boolean Element of BOOLEAN
(u . x1) '&' (a . x1) is V39() boolean Element of BOOLEAN
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
u . z is V39() boolean Element of BOOLEAN
TRUE '&' TRUE is V39() boolean Element of BOOLEAN
z is Element of Y
(u '&' (Y,a,G,PA)) . z is V39() boolean Element of BOOLEAN
(Y,(u '&' a),G,PA) . z is V39() boolean Element of BOOLEAN
u . z is V39() boolean Element of BOOLEAN
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
(u . z) '&' ((Y,a,G,PA) . z) is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
(u '&' a) . x1 is V39() boolean Element of BOOLEAN
TRUE '&' TRUE is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
PA is non empty with_non-empty_elements a_partition of Y
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a '&' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,(a '&' u),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_SUP ((a '&' u),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_SUP (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) '&' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'imp' a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is non empty with_non-empty_elements a_partition of Y
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_SUP (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'imp' (Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,(u 'imp' a),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_SUP ((u 'imp' a),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
(u 'imp' (Y,a,G,PA)) . z is V39() boolean Element of BOOLEAN
(Y,(u 'imp' a),G,PA) . z is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
u . z is V39() boolean Element of BOOLEAN
'not' (u . z) is V39() boolean Element of BOOLEAN
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
('not' (u . z)) 'or' ((Y,a,G,PA) . z) is V39() boolean set
'not' ('not' (u . z)) is V39() boolean set
'not' ((Y,a,G,PA) . z) is V39() boolean set
('not' ('not' (u . z))) '&' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (('not' ('not' (u . z))) '&' ('not' ((Y,a,G,PA) . z))) is V39() boolean set
(u 'imp' a) . z is V39() boolean Element of BOOLEAN
a . z is V39() boolean Element of BOOLEAN
('not' (u . z)) 'or' (a . z) is V39() boolean set
'not' (a . z) is V39() boolean set
('not' ('not' (u . z))) '&' ('not' (a . z)) is V39() boolean set
'not' (('not' ('not' (u . z))) '&' ('not' (a . z))) is V39() boolean set
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
(u 'imp' a) . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
'not' (u . x1) is V39() boolean Element of BOOLEAN
('not' (u . x1)) 'or' (a . x1) is V39() boolean set
'not' ('not' (u . x1)) is V39() boolean set
'not' (a . x1) is V39() boolean set
('not' ('not' (u . x1))) '&' ('not' (a . x1)) is V39() boolean set
'not' (('not' ('not' (u . x1))) '&' ('not' (a . x1))) is V39() boolean set
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'imp' a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is non empty with_non-empty_elements a_partition of Y
(Y,u,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_SUP (u,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,u,G,PA) 'imp' a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,(u 'imp' a),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_SUP ((u 'imp' a),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
((Y,u,G,PA) 'imp' a) . z is V39() boolean Element of BOOLEAN
(Y,(u 'imp' a),G,PA) . z is V39() boolean Element of BOOLEAN
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
(Y,u,G,PA) . z is V39() boolean Element of BOOLEAN
'not' ((Y,u,G,PA) . z) is V39() boolean Element of BOOLEAN
a . z is V39() boolean Element of BOOLEAN
('not' ((Y,u,G,PA) . z)) 'or' (a . z) is V39() boolean set
'not' ('not' ((Y,u,G,PA) . z)) is V39() boolean set
'not' (a . z) is V39() boolean set
('not' ('not' ((Y,u,G,PA) . z))) '&' ('not' (a . z)) is V39() boolean set
'not' (('not' ('not' ((Y,u,G,PA) . z))) '&' ('not' (a . z))) is V39() boolean set
u . z is V39() boolean Element of BOOLEAN
(u 'imp' a) . z is V39() boolean Element of BOOLEAN
'not' (u . z) is V39() boolean Element of BOOLEAN
('not' (u . z)) 'or' (a . z) is V39() boolean set
'not' ('not' (u . z)) is V39() boolean set
('not' ('not' (u . z))) '&' ('not' (a . z)) is V39() boolean set
'not' (('not' ('not' (u . z))) '&' ('not' (a . z))) is V39() boolean set
TRUE 'or' (a . z) is V39() boolean set
'not' TRUE is V39() boolean set
('not' TRUE) '&' ('not' (a . z)) is V39() boolean set
'not' (('not' TRUE) '&' ('not' (a . z))) is V39() boolean set
(u 'imp' a) . z is V39() boolean Element of BOOLEAN
u . z is V39() boolean Element of BOOLEAN
'not' (u . z) is V39() boolean Element of BOOLEAN
('not' (u . z)) 'or' (a . z) is V39() boolean set
'not' ('not' (u . z)) is V39() boolean set
('not' ('not' (u . z))) '&' ('not' (a . z)) is V39() boolean set
'not' (('not' ('not' (u . z))) '&' ('not' (a . z))) is V39() boolean set
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
G is Element of bool (PARTITIONS Y)
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'xor' a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
PA is non empty with_non-empty_elements a_partition of Y
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_SUP (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
u 'xor' (Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,(u 'xor' a),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_SUP ((u 'xor' a),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' FALSE is V39() boolean Element of BOOLEAN
z is Element of Y
(u 'xor' (Y,a,G,PA)) . z is V39() boolean Element of BOOLEAN
(Y,(u 'xor' a),G,PA) . z is V39() boolean Element of BOOLEAN
u . z is V39() boolean Element of BOOLEAN
(Y,a,G,PA) . z is V39() boolean Element of BOOLEAN
(u . z) 'xor' ((Y,a,G,PA) . z) is V39() boolean set
(u . z) <=> ((Y,a,G,PA) . z) is V39() boolean set
'not' ((u . z) 'xor' ((Y,a,G,PA) . z)) is V39() boolean set
(u . z) => ((Y,a,G,PA) . z) is V39() boolean set
'not' (u . z) is V39() boolean set
('not' (u . z)) 'or' ((Y,a,G,PA) . z) is V39() boolean set
'not' ('not' (u . z)) is V39() boolean set
'not' ((Y,a,G,PA) . z) is V39() boolean set
('not' ('not' (u . z))) '&' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (('not' ('not' (u . z))) '&' ('not' ((Y,a,G,PA) . z))) is V39() boolean set
((Y,a,G,PA) . z) => (u . z) is V39() boolean set
('not' ((Y,a,G,PA) . z)) 'or' (u . z) is V39() boolean set
'not' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
('not' ('not' ((Y,a,G,PA) . z))) '&' ('not' (u . z)) is V39() boolean set
'not' (('not' ('not' ((Y,a,G,PA) . z))) '&' ('not' (u . z))) is V39() boolean set
((u . z) => ((Y,a,G,PA) . z)) '&' (((Y,a,G,PA) . z) => (u . z)) is V39() boolean set
'not' ((u . z) <=> ((Y,a,G,PA) . z)) is V39() boolean set
'not' (u . z) is V39() boolean Element of BOOLEAN
('not' (u . z)) '&' ((Y,a,G,PA) . z) is V39() boolean Element of BOOLEAN
'not' ((Y,a,G,PA) . z) is V39() boolean Element of BOOLEAN
(u . z) '&' ('not' ((Y,a,G,PA) . z)) is V39() boolean Element of BOOLEAN
(('not' (u . z)) '&' ((Y,a,G,PA) . z)) 'or' ((u . z) '&' ('not' ((Y,a,G,PA) . z))) is V39() boolean set
'not' (('not' (u . z)) '&' ((Y,a,G,PA) . z)) is V39() boolean set
'not' ((u . z) '&' ('not' ((Y,a,G,PA) . z))) is V39() boolean set
('not' (('not' (u . z)) '&' ((Y,a,G,PA) . z))) '&' ('not' ((u . z) '&' ('not' ((Y,a,G,PA) . z)))) is V39() boolean set
'not' (('not' (('not' (u . z)) '&' ((Y,a,G,PA) . z))) '&' ('not' ((u . z) '&' ('not' ((Y,a,G,PA) . z))))) is V39() boolean set
EqClass (z,(Y,PA,G)) is Element of (Y,PA,G)
x1 is Element of Y
a . x1 is V39() boolean Element of BOOLEAN
u . x1 is V39() boolean Element of BOOLEAN
(u 'xor' a) . x1 is V39() boolean Element of BOOLEAN
(u . x1) 'xor' (a . x1) is V39() boolean set
(u . x1) <=> (a . x1) is V39() boolean set
'not' ((u . x1) 'xor' (a . x1)) is V39() boolean set
(u . x1) => (a . x1) is V39() boolean set
'not' (u . x1) is V39() boolean set
('not' (u . x1)) 'or' (a . x1) is V39() boolean set
'not' ('not' (u . x1)) is V39() boolean set
'not' (a . x1) is V39() boolean set
('not' ('not' (u . x1))) '&' ('not' (a . x1)) is V39() boolean set
'not' (('not' ('not' (u . x1))) '&' ('not' (a . x1))) is V39() boolean set
(a . x1) => (u . x1) is V39() boolean set
('not' (a . x1)) 'or' (u . x1) is V39() boolean set
'not' ('not' (a . x1)) is V39() boolean set
('not' ('not' (a . x1))) '&' ('not' (u . x1)) is V39() boolean set
'not' (('not' ('not' (a . x1))) '&' ('not' (u . x1))) is V39() boolean set
((u . x1) => (a . x1)) '&' ((a . x1) => (u . x1)) is V39() boolean set
'not' ((u . x1) <=> (a . x1)) is V39() boolean set
TRUE 'or' FALSE is V39() boolean set
'not' TRUE is V39() boolean set
'not' FALSE is V39() boolean set
('not' TRUE) '&' ('not' FALSE) is V39() boolean set
'not' (('not' TRUE) '&' ('not' FALSE)) is V39() boolean set
a . z is V39() boolean Element of BOOLEAN
(u 'xor' a) . z is V39() boolean Element of BOOLEAN
(u . z) 'xor' (a . z) is V39() boolean set
(u . z) <=> (a . z) is V39() boolean set
'not' ((u . z) 'xor' (a . z)) is V39() boolean set
(u . z) => (a . z) is V39() boolean set
('not' (u . z)) 'or' (a . z) is V39() boolean set
'not' (a . z) is V39() boolean set
('not' ('not' (u . z))) '&' ('not' (a . z)) is V39() boolean set
'not' (('not' ('not' (u . z))) '&' ('not' (a . z))) is V39() boolean set
(a . z) => (u . z) is V39() boolean set
('not' (a . z)) 'or' (u . z) is V39() boolean set
'not' ('not' (a . z)) is V39() boolean set
('not' ('not' (a . z))) '&' ('not' (u . z)) is V39() boolean set
'not' (('not' ('not' (a . z))) '&' ('not' (u . z))) is V39() boolean set
((u . z) => (a . z)) '&' ((a . z) => (u . z)) is V39() boolean set
'not' ((u . z) <=> (a . z)) is V39() boolean set
FALSE 'or' TRUE is V39() boolean set
'not' FALSE is V39() boolean set
'not' TRUE is V39() boolean set
('not' FALSE) '&' ('not' TRUE) is V39() boolean set
'not' (('not' FALSE) '&' ('not' TRUE)) is V39() boolean set
Y is non empty set
PARTITIONS Y is non empty set
bool (PARTITIONS Y) is non empty set
[:Y,BOOLEAN:] is non empty set
bool [:Y,BOOLEAN:] is non empty set
u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
PA is non empty with_non-empty_elements a_partition of Y
a is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,PA,G) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty partition-membered Element of bool (bool (bool Y))
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
(Y,PA) is non empty Element of bool (Y)
bool (Y) is non empty set
G \ (Y,PA) is Element of bool (Y)
(Y,(G \ (Y,PA))) is non empty with_non-empty_elements a_partition of Y
B_SUP (a,(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,a,G,PA) 'xor' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
a 'xor' u is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Y,(a 'xor' u),G,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B_SUP ((a 'xor' u),(Y,PA,G)) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]