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

K121() is empty V55() Element of K120()

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

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

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

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

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

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

dom z is set
rng z is set
x1 is Element of bool (bool Y)
Intersect x1 is Element of bool Y

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 () is non empty set
bool Y is non empty set
G is Element of bool ()
u is Element of Y
bool (bool Y) is non empty set
{ b1 where b1 is Element of bool Y : S1[b1] } 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
meet PA is Element of bool Y
x /\ x is Element of bool Y
x /\ (x `) is Element of bool Y
x /\ () 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)

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

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

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

Y is non empty set
is non empty set
bool 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

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

Y is non empty set
PARTITIONS Y is non empty set
bool () is non empty set
is non empty set
bool is non empty set
G is Element of bool ()

a is non empty with_non-empty_elements a_partition of Y

(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

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
u . ad is V39() boolean Element of BOOLEAN
x is Element of Y
u . x is V39() boolean Element of BOOLEAN
u . ad is V39() boolean Element of BOOLEAN
x is Element of Y
u . x is V39() boolean Element of BOOLEAN
u . ad is V39() boolean Element of BOOLEAN
g is Element of Y
u . g is V39() boolean Element of BOOLEAN
c13 is Element of Y
u . c13 is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool () is non empty set
is non empty set
bool is non empty set
G is Element of bool ()

a is non empty with_non-empty_elements a_partition of Y

(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

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
u . ad is V39() boolean Element of BOOLEAN
x is Element of Y
u . x is V39() boolean Element of BOOLEAN
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
u . ad is V39() boolean Element of BOOLEAN
g is Element of Y
u . g is V39() boolean Element of BOOLEAN
c13 is Element of Y
u . c13 is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool () is non empty set
is non empty set
bool is non empty set

G is Element of bool ()
a is non empty with_non-empty_elements a_partition of Y

(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

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

G is Element of bool ()
a is non empty with_non-empty_elements a_partition of Y

(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

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

G is Element of bool ()
a is non empty with_non-empty_elements a_partition of Y

(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

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

G is Element of bool ()
a is non empty with_non-empty_elements a_partition of Y

(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

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

a is non empty with_non-empty_elements a_partition of Y

(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

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

a is non empty with_non-empty_elements a_partition of Y

(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

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

PA is non empty with_non-empty_elements a_partition of Y

(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

(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

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' (a . x1)) is V39() boolean set
'not' (() '&' ('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' (u . x1)) '&' () is V39() boolean set
'not' (('not' (u . x1)) '&' ()) is V39() boolean set
Y is non empty set
PARTITIONS Y is non empty set
bool () is non empty set
is non empty set
bool is non empty set
G is Element of bool ()

PA is non empty with_non-empty_elements a_partition of Y

(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

(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
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' ('not' ((Y,u,G,PA) . z))) '&' () is V39() boolean set
'not' (('not' ('not' ((Y,u,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
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' () is V39() boolean set

() '&' () is V39() boolean set
'not' (() '&' ()) is V39() boolean set

() '&' () is V39() boolean set
'not' (() '&' ()) 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' ('not' ((Y,u,G,PA) . z))) '&' () is V39() boolean set
'not' (('not' ('not' ((Y,u,G,PA) . 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)
TRUE 'or' ((Y,a,G,PA) . z) is V39() boolean set

() '&' ('not' ((Y,a,G,PA) . z)) is V39() boolean set
'not' (() '&' ('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
is non empty set
bool 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

a is Element of bool (Y)
PA is non empty with_non-empty_elements a_partition of Y

(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

(Y,G,a,PA) '&' (Y,u,a,PA) is Relation-like Y -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of bool
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

Y is non empty set
PARTITIONS Y is non empty set
bool () is non empty set
is non empty set
bool is non empty set
G is Element of bool ()

PA is non empty with_non-empty_elements a_partition of Y

(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

(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

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

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

() '&' () is V39() boolean set
'not' (() '&' ()) 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

() '&' () is V39() boolean set
'not' (() '&' ()) is V39() boolean set
Y is non empty set
PARTITIONS Y is non empty set
bool () is non empty set
is non empty set
bool is non empty set
G is Element of bool ()

PA is non empty with_non-empty_elements a_partition of Y

(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

(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

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' (a . z)) is V39() boolean set
'not' (() '&' ('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 () is non empty set
is non empty set
bool is non empty set
G is Element of bool ()

a is non empty with_non-empty_elements a_partition of Y

(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

PA is Element of Y
('not' (Y,u,G,a)) . PA is V39() boolean set
(Y,(),G,a) . PA is V39() boolean set
EqClass (PA,(Y,a,G)) is Element of (Y,a,G)
z is Element of Y
() . z is V39() boolean Element of BOOLEAN
z is Element of Y
() . 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
() . 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)))) . PA is V39() boolean Element of BOOLEAN

(B_SUP ((),(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
() . x1 is V39() boolean Element of BOOLEAN

('not' (B_INF (u,(Y,a,G)))) . PA is V39() boolean Element of BOOLEAN

(B_SUP ((),(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
() . 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
() . 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
() . x2 is V39() boolean Element of BOOLEAN
x2 is Element of Y
() . x2 is V39() boolean Element of BOOLEAN
Y is non empty set
PARTITIONS Y is non empty set
bool () is non empty set
is non empty set
bool is non empty set
G is Element of bool ()

a is non empty with_non-empty_elements a_partition of Y

(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

PA is Element of Y
('not' (Y,u,G,a)) . PA is V39() boolean set
(Y,(),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
() . 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)
(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)))) . 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
() . 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)))) . PA is V39() boolean Element of BOOLEAN

(B_INF ((),(Y,a,G))) . PA is V39() boolean Element of BOOLEAN
z is Element of Y
() . 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
() . z is V39() boolean Element of BOOLEAN
z is Element of Y
() . 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
() . x1 is V39() boolean Element of BOOLEAN
EqClass (PA,(Y,a,G)) is Element of (Y,a,G)
z is Element of Y
() . z is V39() boolean Element of BOOLEAN
x1 is Element of Y
() . 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 () is non empty set
is non empty set
bool is non empty set
G is Element of bool ()

PA is non empty with_non-empty_elements a_partition of Y

(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

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' ('not' (u . x1))) '&' () is V39() boolean set
'not' (('not' ('not' (u . x1))) '&' ()) 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' () is V39() boolean set

() '&' () is V39() boolean set
'not' (() '&' ()) is V39() boolean set

() '&' () is V39() boolean set
'not' (() '&' ()) 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 () is non empty set
is non empty set
bool is non empty set
G is Element of bool ()

PA is non empty with_non-empty_elements a_partition of Y

(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

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
<