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

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

u . c

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

u . c

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

<