:: BVFUNC_3 semantic presentation

K114() is Element of K10(K110())

K110() is set

K10(K110()) is set

K109() is set

K10(K109()) is set

K10(K114()) is set

BOOLEAN is non empty set

FALSE is boolean Element of BOOLEAN

K115() is empty V55() Element of K114()

TRUE is boolean Element of BOOLEAN

1 is non empty set

FALSE is set

TRUE is set

Y is non empty set

PARTITIONS Y is partition-membered Element of K10(K10(K32(Y)))

K32(Y) is Element of K10(K10(Y))

K10(Y) is set

K10(K10(Y)) is set

K10(K32(Y)) is set

K10(K10(K32(Y))) is set

K10((PARTITIONS Y)) is set

K11(Y,BOOLEAN) is set

K10(K11(Y,BOOLEAN)) is set

G is Element of K10((PARTITIONS Y))

c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

c 'imp' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

a is a_partition of Y

All (c,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex (b,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(All (c,a,G)) 'imp' (Ex (b,a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

PA is Element of Y

(c 'imp' b) . PA is boolean Element of BOOLEAN

((All (c,a,G)) 'imp' (Ex (b,a,G))) . PA is boolean Element of BOOLEAN

c . PA is boolean Element of BOOLEAN

'not' (c . PA) is boolean Element of BOOLEAN

CompF (a,G) is a_partition of Y

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

b . PA is boolean Element of BOOLEAN

('not' (c . PA)) 'or' (b . PA) is set

'not' ('not' (c . PA)) is boolean set

'not' (b . PA) is boolean set

('not' ('not' (c . PA))) '&' ('not' (b . PA)) is set

'not' (('not' ('not' (c . PA))) '&' ('not' (b . PA))) is boolean set

B_INF (c,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_INF (c,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

(All (c,a,G)) . PA is boolean Element of BOOLEAN

'not' FALSE is boolean Element of BOOLEAN

(Ex (b,a,G)) . PA is boolean Element of BOOLEAN

('not' FALSE) 'or' ((Ex (b,a,G)) . PA) is set

'not' ('not' FALSE) is boolean set

'not' ((Ex (b,a,G)) . PA) is boolean set

('not' ('not' FALSE)) '&' ('not' ((Ex (b,a,G)) . PA)) is set

'not' (('not' ('not' FALSE)) '&' ('not' ((Ex (b,a,G)) . PA))) is boolean set

TRUE 'or' ((Ex (b,a,G)) . PA) is set

'not' TRUE is boolean set

('not' TRUE) '&' ('not' ((Ex (b,a,G)) . PA)) is set

'not' (('not' TRUE) '&' ('not' ((Ex (b,a,G)) . PA))) is boolean set

B_SUP (b,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_SUP (b,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

(Ex (b,a,G)) . PA is boolean Element of BOOLEAN

(All (c,a,G)) . PA is boolean Element of BOOLEAN

'not' ((All (c,a,G)) . PA) is boolean Element of BOOLEAN

('not' ((All (c,a,G)) . PA)) 'or' TRUE is set

'not' ('not' ((All (c,a,G)) . PA)) is boolean set

'not' TRUE is boolean set

('not' ('not' ((All (c,a,G)) . PA))) '&' ('not' TRUE) is set

'not' (('not' ('not' ((All (c,a,G)) . PA))) '&' ('not' TRUE)) is boolean set

Y is non empty set

PARTITIONS Y is partition-membered Element of K10(K10(K32(Y)))

K32(Y) is Element of K10(K10(Y))

K10(Y) is set

K10(K10(Y)) is set

K10(K32(Y)) is set

K10(K10(K32(Y))) is set

K10((PARTITIONS Y)) is set

K11(Y,BOOLEAN) is set

K10(K11(Y,BOOLEAN)) is set

G is Element of K10((PARTITIONS Y))

c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

c '&' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

a is a_partition of Y

All (c,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

All (b,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(All (c,a,G)) '&' (All (b,a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

PA is Element of Y

((All (c,a,G)) '&' (All (b,a,G))) . PA is boolean Element of BOOLEAN

(c '&' b) . PA is boolean Element of BOOLEAN

(All (c,a,G)) . PA is boolean Element of BOOLEAN

(All (b,a,G)) . PA is boolean Element of BOOLEAN

((All (c,a,G)) . PA) '&' ((All (b,a,G)) . PA) is boolean Element of BOOLEAN

CompF (a,G) is a_partition of Y

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

B_INF (c,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_INF (c,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

z is Element of Y

c . z is boolean Element of BOOLEAN

B_INF (b,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_INF (b,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

z is Element of Y

b . z is boolean Element of BOOLEAN

b . PA is boolean Element of BOOLEAN

c . PA is boolean Element of BOOLEAN

(c . PA) '&' (b . PA) is boolean Element of BOOLEAN

TRUE '&' TRUE is boolean Element of BOOLEAN

Y is non empty set

PARTITIONS Y is partition-membered Element of K10(K10(K32(Y)))

K32(Y) is Element of K10(K10(Y))

K10(Y) is set

K10(K10(Y)) is set

K10(K32(Y)) is set

K10(K10(K32(Y))) is set

K10((PARTITIONS Y)) is set

K11(Y,BOOLEAN) is set

K10(K11(Y,BOOLEAN)) is set

G is Element of K10((PARTITIONS Y))

c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

c '&' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

a is a_partition of Y

Ex (c,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex (b,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(Ex (c,a,G)) '&' (Ex (b,a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

PA is Element of Y

(c '&' b) . PA is boolean Element of BOOLEAN

((Ex (c,a,G)) '&' (Ex (b,a,G))) . PA is boolean Element of BOOLEAN

c . PA is boolean Element of BOOLEAN

b . PA is boolean Element of BOOLEAN

(c . PA) '&' (b . PA) is boolean Element of BOOLEAN

CompF (a,G) is a_partition of Y

B_SUP (c,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

B_SUP (b,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_SUP (b,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

(Ex (b,a,G)) . PA is boolean Element of BOOLEAN

(Ex (c,a,G)) . PA is boolean Element of BOOLEAN

((Ex (c,a,G)) . PA) '&' ((Ex (b,a,G)) . PA) is boolean Element of BOOLEAN

TRUE '&' TRUE is boolean Element of BOOLEAN

Y is non empty set

PARTITIONS Y is partition-membered Element of K10(K10(K32(Y)))

K32(Y) is Element of K10(K10(Y))

K10(Y) is set

K10(K10(Y)) is set

K10(K32(Y)) is set

K10(K10(K32(Y))) is set

K10((PARTITIONS Y)) is set

K11(Y,BOOLEAN) is set

K10(K11(Y,BOOLEAN)) is set

G is Element of K10((PARTITIONS Y))

c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

'not' c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

'not' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

a is a_partition of Y

All (c,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

All (b,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(All (c,a,G)) '&' (All (b,a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

'not' ((All (c,a,G)) '&' (All (b,a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex (('not' c),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex (('not' b),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(Ex (('not' c),a,G)) 'or' (Ex (('not' b),a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

CompF (a,G) is a_partition of Y

B_INF (b,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

B_INF (c,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

PA is Element of Y

((Ex (('not' c),a,G)) 'or' (Ex (('not' b),a,G))) . PA is boolean Element of BOOLEAN

('not' ((All (c,a,G)) '&' (All (b,a,G)))) . PA is boolean Element of BOOLEAN

(Ex (('not' c),a,G)) . PA is boolean Element of BOOLEAN

(Ex (('not' b),a,G)) . PA is boolean Element of BOOLEAN

((Ex (('not' c),a,G)) . PA) 'or' ((Ex (('not' b),a,G)) . PA) is set

'not' ((Ex (('not' c),a,G)) . PA) is boolean set

'not' ((Ex (('not' b),a,G)) . PA) is boolean set

('not' ((Ex (('not' c),a,G)) . PA)) '&' ('not' ((Ex (('not' b),a,G)) . PA)) is set

'not' (('not' ((Ex (('not' c),a,G)) . PA)) '&' ('not' ((Ex (('not' b),a,G)) . PA))) is boolean set

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

B_SUP (('not' c),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_SUP (('not' c),(CompF (a,G)))) . PA is boolean Element of BOOLEAN

z is Element of Y

('not' c) . z is boolean Element of BOOLEAN

z is Element of Y

('not' c) . z is boolean Element of BOOLEAN

c . z is boolean Element of BOOLEAN

'not' (c . z) is boolean Element of BOOLEAN

((All (c,a,G)) '&' (All (b,a,G))) . PA is boolean Element of BOOLEAN

'not' (((All (c,a,G)) '&' (All (b,a,G))) . PA) is boolean Element of BOOLEAN

(All (c,a,G)) . PA is boolean Element of BOOLEAN

(All (b,a,G)) . PA is boolean Element of BOOLEAN

((All (c,a,G)) . PA) '&' ((All (b,a,G)) . PA) is boolean Element of BOOLEAN

'not' (((All (c,a,G)) . PA) '&' ((All (b,a,G)) . PA)) is boolean Element of BOOLEAN

FALSE '&' ((All (b,a,G)) . PA) is boolean Element of BOOLEAN

'not' (FALSE '&' ((All (b,a,G)) . PA)) is boolean Element of BOOLEAN

'not' FALSE is boolean Element of BOOLEAN

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

B_SUP (('not' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_SUP (('not' b),(CompF (a,G)))) . PA is boolean Element of BOOLEAN

z is Element of Y

('not' b) . z is boolean Element of BOOLEAN

z is Element of Y

('not' b) . z is boolean Element of BOOLEAN

b . z is boolean Element of BOOLEAN

'not' (b . z) is boolean Element of BOOLEAN

((All (c,a,G)) '&' (All (b,a,G))) . PA is boolean Element of BOOLEAN

'not' (((All (c,a,G)) '&' (All (b,a,G))) . PA) is boolean Element of BOOLEAN

(All (c,a,G)) . PA is boolean Element of BOOLEAN

(All (b,a,G)) . PA is boolean Element of BOOLEAN

((All (c,a,G)) . PA) '&' ((All (b,a,G)) . PA) is boolean Element of BOOLEAN

'not' (((All (c,a,G)) . PA) '&' ((All (b,a,G)) . PA)) is boolean Element of BOOLEAN

((All (c,a,G)) . PA) '&' FALSE is boolean Element of BOOLEAN

'not' (((All (c,a,G)) . PA) '&' FALSE) is boolean Element of BOOLEAN

'not' FALSE is boolean Element of BOOLEAN

PA is Element of Y

('not' ((All (c,a,G)) '&' (All (b,a,G)))) . PA is boolean Element of BOOLEAN

((Ex (('not' c),a,G)) 'or' (Ex (('not' b),a,G))) . PA is boolean Element of BOOLEAN

((All (c,a,G)) '&' (All (b,a,G))) . PA is boolean Element of BOOLEAN

'not' (((All (c,a,G)) '&' (All (b,a,G))) . PA) is boolean Element of BOOLEAN

(All (c,a,G)) . PA is boolean Element of BOOLEAN

(All (b,a,G)) . PA is boolean Element of BOOLEAN

((All (c,a,G)) . PA) '&' ((All (b,a,G)) . PA) is boolean Element of BOOLEAN

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

z is Element of Y

c . z is boolean Element of BOOLEAN

'not' (c . z) is boolean Element of BOOLEAN

('not' c) . z is boolean Element of BOOLEAN

B_SUP (('not' c),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_SUP (('not' c),(CompF (a,G)))) . PA is boolean Element of BOOLEAN

(Ex (('not' c),a,G)) . PA is boolean Element of BOOLEAN

(Ex (('not' b),a,G)) . PA is boolean Element of BOOLEAN

TRUE 'or' ((Ex (('not' b),a,G)) . PA) is set

'not' TRUE is boolean set

'not' ((Ex (('not' b),a,G)) . PA) is boolean set

('not' TRUE) '&' ('not' ((Ex (('not' b),a,G)) . PA)) is set

'not' (('not' TRUE) '&' ('not' ((Ex (('not' b),a,G)) . PA))) is boolean set

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

z is Element of Y

b . z is boolean Element of BOOLEAN

'not' (b . z) is boolean Element of BOOLEAN

('not' b) . z is boolean Element of BOOLEAN

B_SUP (('not' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_SUP (('not' b),(CompF (a,G)))) . PA is boolean Element of BOOLEAN

(Ex (('not' b),a,G)) . PA is boolean Element of BOOLEAN

(Ex (('not' c),a,G)) . PA is boolean Element of BOOLEAN

((Ex (('not' c),a,G)) . PA) 'or' TRUE is set

'not' ((Ex (('not' c),a,G)) . PA) is boolean set

'not' TRUE is boolean set

('not' ((Ex (('not' c),a,G)) . PA)) '&' ('not' TRUE) is set

'not' (('not' ((Ex (('not' c),a,G)) . PA)) '&' ('not' TRUE)) is boolean set

Y is non empty set

PARTITIONS Y is partition-membered Element of K10(K10(K32(Y)))

K32(Y) is Element of K10(K10(Y))

K10(Y) is set

K10(K10(Y)) is set

K10(K32(Y)) is set

K10(K10(K32(Y))) is set

K10((PARTITIONS Y)) is set

K11(Y,BOOLEAN) is set

K10(K11(Y,BOOLEAN)) is set

G is Element of K10((PARTITIONS Y))

c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

'not' c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

'not' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

a is a_partition of Y

Ex (c,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex (b,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(Ex (c,a,G)) '&' (Ex (b,a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

'not' ((Ex (c,a,G)) '&' (Ex (b,a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

All (('not' c),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

All (('not' b),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(All (('not' c),a,G)) 'or' (All (('not' b),a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

CompF (a,G) is a_partition of Y

B_INF (('not' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

B_SUP (b,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

B_SUP (c,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

PA is Element of Y

((All (('not' c),a,G)) 'or' (All (('not' b),a,G))) . PA is boolean Element of BOOLEAN

('not' ((Ex (c,a,G)) '&' (Ex (b,a,G)))) . PA is boolean Element of BOOLEAN

(All (('not' b),a,G)) . PA is boolean Element of BOOLEAN

(All (('not' c),a,G)) . PA is boolean Element of BOOLEAN

((All (('not' c),a,G)) . PA) 'or' ((All (('not' b),a,G)) . PA) is set

'not' ((All (('not' c),a,G)) . PA) is boolean set

'not' ((All (('not' b),a,G)) . PA) is boolean set

('not' ((All (('not' c),a,G)) . PA)) '&' ('not' ((All (('not' b),a,G)) . PA)) is set

'not' (('not' ((All (('not' c),a,G)) . PA)) '&' ('not' ((All (('not' b),a,G)) . PA))) is boolean set

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

B_INF (('not' c),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_INF (('not' c),(CompF (a,G)))) . PA is boolean Element of BOOLEAN

z is Element of Y

('not' c) . z is boolean Element of BOOLEAN

z is Element of Y

('not' c) . z is boolean Element of BOOLEAN

c . z is boolean Element of BOOLEAN

'not' (c . z) is boolean Element of BOOLEAN

((Ex (c,a,G)) '&' (Ex (b,a,G))) . PA is boolean Element of BOOLEAN

'not' (((Ex (c,a,G)) '&' (Ex (b,a,G))) . PA) is boolean Element of BOOLEAN

(Ex (c,a,G)) . PA is boolean Element of BOOLEAN

(Ex (b,a,G)) . PA is boolean Element of BOOLEAN

((Ex (c,a,G)) . PA) '&' ((Ex (b,a,G)) . PA) is boolean Element of BOOLEAN

'not' (((Ex (c,a,G)) . PA) '&' ((Ex (b,a,G)) . PA)) is boolean Element of BOOLEAN

FALSE '&' ((Ex (b,a,G)) . PA) is boolean Element of BOOLEAN

'not' (FALSE '&' ((Ex (b,a,G)) . PA)) is boolean Element of BOOLEAN

'not' FALSE is boolean Element of BOOLEAN

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

(B_INF (('not' b),(CompF (a,G)))) . PA is boolean Element of BOOLEAN

z is Element of Y

('not' b) . z is boolean Element of BOOLEAN

z is Element of Y

('not' b) . z is boolean Element of BOOLEAN

b . z is boolean Element of BOOLEAN

'not' (b . z) is boolean Element of BOOLEAN

((Ex (c,a,G)) '&' (Ex (b,a,G))) . PA is boolean Element of BOOLEAN

'not' (((Ex (c,a,G)) '&' (Ex (b,a,G))) . PA) is boolean Element of BOOLEAN

(Ex (c,a,G)) . PA is boolean Element of BOOLEAN

(Ex (b,a,G)) . PA is boolean Element of BOOLEAN

((Ex (c,a,G)) . PA) '&' ((Ex (b,a,G)) . PA) is boolean Element of BOOLEAN

'not' (((Ex (c,a,G)) . PA) '&' ((Ex (b,a,G)) . PA)) is boolean Element of BOOLEAN

((Ex (c,a,G)) . PA) '&' FALSE is boolean Element of BOOLEAN

'not' (((Ex (c,a,G)) . PA) '&' FALSE) is boolean Element of BOOLEAN

'not' FALSE is boolean Element of BOOLEAN

B_INF (('not' c),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

PA is Element of Y

('not' ((Ex (c,a,G)) '&' (Ex (b,a,G)))) . PA is boolean Element of BOOLEAN

((All (('not' c),a,G)) 'or' (All (('not' b),a,G))) . PA is boolean Element of BOOLEAN

((Ex (c,a,G)) '&' (Ex (b,a,G))) . PA is boolean Element of BOOLEAN

'not' (((Ex (c,a,G)) '&' (Ex (b,a,G))) . PA) is boolean Element of BOOLEAN

(Ex (c,a,G)) . PA is boolean Element of BOOLEAN

(Ex (b,a,G)) . PA is boolean Element of BOOLEAN

((Ex (c,a,G)) . PA) '&' ((Ex (b,a,G)) . PA) is boolean Element of BOOLEAN

z is Element of Y

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

c . z is boolean Element of BOOLEAN

'not' (c . z) is boolean Element of BOOLEAN

('not' c) . z is boolean Element of BOOLEAN

(All (('not' c),a,G)) . PA is boolean Element of BOOLEAN

(All (('not' b),a,G)) . PA is boolean Element of BOOLEAN

((All (('not' c),a,G)) . PA) 'or' ((All (('not' b),a,G)) . PA) is set

'not' ((All (('not' c),a,G)) . PA) is boolean set

'not' ((All (('not' b),a,G)) . PA) is boolean set

('not' ((All (('not' c),a,G)) . PA)) '&' ('not' ((All (('not' b),a,G)) . PA)) is set

'not' (('not' ((All (('not' c),a,G)) . PA)) '&' ('not' ((All (('not' b),a,G)) . PA))) is boolean set

TRUE 'or' ((All (('not' b),a,G)) . PA) is set

'not' TRUE is boolean set

('not' TRUE) '&' ('not' ((All (('not' b),a,G)) . PA)) is set

'not' (('not' TRUE) '&' ('not' ((All (('not' b),a,G)) . PA))) is boolean set

z is Element of Y

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

b . z is boolean Element of BOOLEAN

'not' (b . z) is boolean Element of BOOLEAN

('not' b) . z is boolean Element of BOOLEAN

(All (('not' c),a,G)) . PA is boolean Element of BOOLEAN

(All (('not' b),a,G)) . PA is boolean Element of BOOLEAN

((All (('not' c),a,G)) . PA) 'or' ((All (('not' b),a,G)) . PA) is set

'not' ((All (('not' c),a,G)) . PA) is boolean set

'not' ((All (('not' b),a,G)) . PA) is boolean set

('not' ((All (('not' c),a,G)) . PA)) '&' ('not' ((All (('not' b),a,G)) . PA)) is set

'not' (('not' ((All (('not' c),a,G)) . PA)) '&' ('not' ((All (('not' b),a,G)) . PA))) is boolean set

((All (('not' c),a,G)) . PA) 'or' TRUE is set

'not' TRUE is boolean set

('not' ((All (('not' c),a,G)) . PA)) '&' ('not' TRUE) is set

'not' (('not' ((All (('not' c),a,G)) . PA)) '&' ('not' TRUE)) is boolean set

Y is non empty set

PARTITIONS Y is partition-membered Element of K10(K10(K32(Y)))

K32(Y) is Element of K10(K10(Y))

K10(Y) is set

K10(K10(Y)) is set

K10(K32(Y)) is set

K10(K10(K32(Y))) is set

K10((PARTITIONS Y)) is set

K11(Y,BOOLEAN) is set

K10(K11(Y,BOOLEAN)) is set

G is Element of K10((PARTITIONS Y))

c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

c 'or' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

a is a_partition of Y

All (c,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

All (b,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(All (c,a,G)) 'or' (All (b,a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

PA is Element of Y

((All (c,a,G)) 'or' (All (b,a,G))) . PA is boolean Element of BOOLEAN

(c 'or' b) . PA is boolean Element of BOOLEAN

(All (c,a,G)) . PA is boolean Element of BOOLEAN

CompF (a,G) is a_partition of Y

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

(All (b,a,G)) . PA is boolean Element of BOOLEAN

((All (c,a,G)) . PA) 'or' ((All (b,a,G)) . PA) is set

'not' ((All (c,a,G)) . PA) is boolean set

'not' ((All (b,a,G)) . PA) is boolean set

('not' ((All (c,a,G)) . PA)) '&' ('not' ((All (b,a,G)) . PA)) is set

'not' (('not' ((All (c,a,G)) . PA)) '&' ('not' ((All (b,a,G)) . PA))) is boolean set

B_INF (c,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_INF (c,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

z is Element of Y

c . z is boolean Element of BOOLEAN

c . PA is boolean Element of BOOLEAN

b . PA is boolean Element of BOOLEAN

(c . PA) 'or' (b . PA) is set

'not' (c . PA) is boolean set

'not' (b . PA) is boolean set

('not' (c . PA)) '&' ('not' (b . PA)) is set

'not' (('not' (c . PA)) '&' ('not' (b . PA))) is boolean set

TRUE 'or' (b . PA) is set

'not' TRUE is boolean set

('not' TRUE) '&' ('not' (b . PA)) is set

'not' (('not' TRUE) '&' ('not' (b . PA))) is boolean set

B_INF (b,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_INF (b,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

z is Element of Y

b . z is boolean Element of BOOLEAN

c . PA is boolean Element of BOOLEAN

b . PA is boolean Element of BOOLEAN

(c . PA) 'or' (b . PA) is set

'not' (c . PA) is boolean set

'not' (b . PA) is boolean set

('not' (c . PA)) '&' ('not' (b . PA)) is set

'not' (('not' (c . PA)) '&' ('not' (b . PA))) is boolean set

(c . PA) 'or' TRUE is set

'not' TRUE is boolean set

('not' (c . PA)) '&' ('not' TRUE) is set

'not' (('not' (c . PA)) '&' ('not' TRUE)) is boolean set

Y is non empty set

PARTITIONS Y is partition-membered Element of K10(K10(K32(Y)))

K32(Y) is Element of K10(K10(Y))

K10(Y) is set

K10(K10(Y)) is set

K10(K32(Y)) is set

K10(K10(K32(Y))) is set

K10((PARTITIONS Y)) is set

K11(Y,BOOLEAN) is set

K10(K11(Y,BOOLEAN)) is set

G is Element of K10((PARTITIONS Y))

c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

c 'or' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

a is a_partition of Y

Ex (c,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex (b,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(Ex (c,a,G)) 'or' (Ex (b,a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

CompF (a,G) is a_partition of Y

B_SUP (c,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

PA is Element of Y

(c 'or' b) . PA is boolean Element of BOOLEAN

((Ex (c,a,G)) 'or' (Ex (b,a,G))) . PA is boolean Element of BOOLEAN

B_SUP (b,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

c . PA is boolean Element of BOOLEAN

b . PA is boolean Element of BOOLEAN

(c . PA) 'or' (b . PA) is set

'not' (c . PA) is boolean set

'not' (b . PA) is boolean set

('not' (c . PA)) '&' ('not' (b . PA)) is set

'not' (('not' (c . PA)) '&' ('not' (b . PA))) is boolean set

(Ex (c,a,G)) . PA is boolean Element of BOOLEAN

(Ex (b,a,G)) . PA is boolean Element of BOOLEAN

((Ex (c,a,G)) . PA) 'or' ((Ex (b,a,G)) . PA) is set

'not' ((Ex (c,a,G)) . PA) is boolean set

'not' ((Ex (b,a,G)) . PA) is boolean set

('not' ((Ex (c,a,G)) . PA)) '&' ('not' ((Ex (b,a,G)) . PA)) is set

'not' (('not' ((Ex (c,a,G)) . PA)) '&' ('not' ((Ex (b,a,G)) . PA))) is boolean set

TRUE 'or' ((Ex (b,a,G)) . PA) is set

'not' TRUE is boolean set

('not' TRUE) '&' ('not' ((Ex (b,a,G)) . PA)) is set

'not' (('not' TRUE) '&' ('not' ((Ex (b,a,G)) . PA))) is boolean set

(Ex (c,a,G)) . PA is boolean Element of BOOLEAN

(Ex (b,a,G)) . PA is boolean Element of BOOLEAN

((Ex (c,a,G)) . PA) 'or' ((Ex (b,a,G)) . PA) is set

'not' ((Ex (c,a,G)) . PA) is boolean set

'not' ((Ex (b,a,G)) . PA) is boolean set

('not' ((Ex (c,a,G)) . PA)) '&' ('not' ((Ex (b,a,G)) . PA)) is set

'not' (('not' ((Ex (c,a,G)) . PA)) '&' ('not' ((Ex (b,a,G)) . PA))) is boolean set

((Ex (c,a,G)) . PA) 'or' TRUE is set

'not' TRUE is boolean set

('not' ((Ex (c,a,G)) . PA)) '&' ('not' TRUE) is set

'not' (('not' ((Ex (c,a,G)) . PA)) '&' ('not' TRUE)) is boolean set

Y is non empty set

PARTITIONS Y is partition-membered Element of K10(K10(K32(Y)))

K32(Y) is Element of K10(K10(Y))

K10(Y) is set

K10(K10(Y)) is set

K10(K32(Y)) is set

K10(K10(K32(Y))) is set

K10((PARTITIONS Y)) is set

K11(Y,BOOLEAN) is set

K10(K11(Y,BOOLEAN)) is set

G is Element of K10((PARTITIONS Y))

c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

'not' c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

c 'xor' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

'not' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

a is a_partition of Y

Ex (('not' c),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex (b,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(Ex (('not' c),a,G)) 'xor' (Ex (b,a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

'not' ((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex (c,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex (('not' b),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(Ex (c,a,G)) 'xor' (Ex (('not' b),a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

'not' ((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

('not' ((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G)))) 'or' ('not' ((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G)))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

CompF (a,G) is a_partition of Y

B_SUP (('not' c),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

PA is Element of Y

(c 'xor' b) . PA is boolean Element of BOOLEAN

(('not' ((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G)))) 'or' ('not' ((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G))))) . PA is boolean Element of BOOLEAN

B_SUP (('not' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

c . PA is boolean Element of BOOLEAN

b . PA is boolean Element of BOOLEAN

'not' (b . PA) is boolean Element of BOOLEAN

(c . PA) '&' ('not' (b . PA)) is boolean Element of BOOLEAN

(c . PA) 'xor' (b . PA) is set

(c . PA) <=> (b . PA) is set

'not' ((c . PA) 'xor' (b . PA)) is boolean set

(c . PA) => (b . PA) is set

'not' (c . PA) is boolean set

('not' (c . PA)) 'or' (b . PA) is set

'not' ('not' (c . PA)) is boolean set

'not' (b . PA) is boolean set

('not' ('not' (c . PA))) '&' ('not' (b . PA)) is set

'not' (('not' ('not' (c . PA))) '&' ('not' (b . PA))) is boolean set

(b . PA) => (c . PA) is set

('not' (b . PA)) 'or' (c . PA) is set

'not' ('not' (b . PA)) is boolean set

('not' ('not' (b . PA))) '&' ('not' (c . PA)) is set

'not' (('not' ('not' (b . PA))) '&' ('not' (c . PA))) is boolean set

((c . PA) => (b . PA)) '&' ((b . PA) => (c . PA)) is set

'not' ((c . PA) <=> (b . PA)) is boolean set

'not' (c . PA) is boolean Element of BOOLEAN

('not' (c . PA)) '&' (b . PA) is boolean Element of BOOLEAN

(('not' (c . PA)) '&' (b . PA)) 'or' ((c . PA) '&' ('not' (b . PA))) is set

'not' (('not' (c . PA)) '&' (b . PA)) is boolean set

'not' ((c . PA) '&' ('not' (b . PA))) is boolean set

('not' (('not' (c . PA)) '&' (b . PA))) '&' ('not' ((c . PA) '&' ('not' (b . PA)))) is set

'not' (('not' (('not' (c . PA)) '&' (b . PA))) '&' ('not' ((c . PA) '&' ('not' (b . PA))))) is boolean set

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

FALSE '&' TRUE is boolean Element of BOOLEAN

('not' c) . PA is boolean Element of BOOLEAN

(B_SUP (('not' c),(CompF (a,G)))) . PA is boolean Element of BOOLEAN

('not' ((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G)))) . PA is boolean Element of BOOLEAN

((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G))) . PA is boolean Element of BOOLEAN

'not' (((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G))) . PA) is boolean Element of BOOLEAN

B_SUP (b,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_SUP (b,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

(Ex (b,a,G)) . PA is boolean Element of BOOLEAN

((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G))) . PA is boolean Element of BOOLEAN

(Ex (('not' c),a,G)) . PA is boolean Element of BOOLEAN

((Ex (('not' c),a,G)) . PA) 'xor' ((Ex (b,a,G)) . PA) is set

((Ex (('not' c),a,G)) . PA) <=> ((Ex (b,a,G)) . PA) is set

'not' (((Ex (('not' c),a,G)) . PA) 'xor' ((Ex (b,a,G)) . PA)) is boolean set

((Ex (('not' c),a,G)) . PA) => ((Ex (b,a,G)) . PA) is set

'not' ((Ex (('not' c),a,G)) . PA) is boolean set

('not' ((Ex (('not' c),a,G)) . PA)) 'or' ((Ex (b,a,G)) . PA) is set

'not' ('not' ((Ex (('not' c),a,G)) . PA)) is boolean set

'not' ((Ex (b,a,G)) . PA) is boolean set

('not' ('not' ((Ex (('not' c),a,G)) . PA))) '&' ('not' ((Ex (b,a,G)) . PA)) is set

'not' (('not' ('not' ((Ex (('not' c),a,G)) . PA))) '&' ('not' ((Ex (b,a,G)) . PA))) is boolean set

((Ex (b,a,G)) . PA) => ((Ex (('not' c),a,G)) . PA) is set

('not' ((Ex (b,a,G)) . PA)) 'or' ((Ex (('not' c),a,G)) . PA) is set

'not' ('not' ((Ex (b,a,G)) . PA)) is boolean set

('not' ('not' ((Ex (b,a,G)) . PA))) '&' ('not' ((Ex (('not' c),a,G)) . PA)) is set

'not' (('not' ('not' ((Ex (b,a,G)) . PA))) '&' ('not' ((Ex (('not' c),a,G)) . PA))) is boolean set

(((Ex (('not' c),a,G)) . PA) => ((Ex (b,a,G)) . PA)) '&' (((Ex (b,a,G)) . PA) => ((Ex (('not' c),a,G)) . PA)) is set

'not' (((Ex (('not' c),a,G)) . PA) <=> ((Ex (b,a,G)) . PA)) is boolean set

('not' ((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G)))) . PA is boolean Element of BOOLEAN

(('not' ((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G)))) . PA) 'or' (('not' ((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G)))) . PA) is set

'not' (('not' ((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G)))) . PA) is boolean set

'not' (('not' ((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G)))) . PA) is boolean set

('not' (('not' ((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G)))) . PA)) '&' ('not' (('not' ((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G)))) . PA)) is set

'not' (('not' (('not' ((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G)))) . PA)) '&' ('not' (('not' ((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G)))) . PA))) is boolean set

'not' FALSE is boolean Element of BOOLEAN

('not' FALSE) 'or' ('not' (((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G))) . PA)) is set

'not' ('not' FALSE) is boolean set

'not' ('not' (((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G))) . PA)) is boolean set

('not' ('not' FALSE)) '&' ('not' ('not' (((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G))) . PA))) is set

'not' (('not' ('not' FALSE)) '&' ('not' ('not' (((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G))) . PA)))) is boolean set

TRUE 'or' ('not' (((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G))) . PA)) is set

'not' TRUE is boolean set

('not' TRUE) '&' ('not' ('not' (((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G))) . PA))) is set

'not' (('not' TRUE) '&' ('not' ('not' (((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G))) . PA)))) is boolean set

B_SUP (c,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_SUP (c,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

(Ex (c,a,G)) . PA is boolean Element of BOOLEAN

('not' ((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G)))) . PA is boolean Element of BOOLEAN

((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G))) . PA is boolean Element of BOOLEAN

'not' (((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G))) . PA) is boolean Element of BOOLEAN

('not' b) . PA is boolean Element of BOOLEAN

(B_SUP (('not' b),(CompF (a,G)))) . PA is boolean Element of BOOLEAN

(Ex (('not' b),a,G)) . PA is boolean Element of BOOLEAN

((Ex (c,a,G)) . PA) 'xor' ((Ex (('not' b),a,G)) . PA) is set

((Ex (c,a,G)) . PA) <=> ((Ex (('not' b),a,G)) . PA) is set

'not' (((Ex (c,a,G)) . PA) 'xor' ((Ex (('not' b),a,G)) . PA)) is boolean set

((Ex (c,a,G)) . PA) => ((Ex (('not' b),a,G)) . PA) is set

'not' ((Ex (c,a,G)) . PA) is boolean set

('not' ((Ex (c,a,G)) . PA)) 'or' ((Ex (('not' b),a,G)) . PA) is set

'not' ('not' ((Ex (c,a,G)) . PA)) is boolean set

'not' ((Ex (('not' b),a,G)) . PA) is boolean set

('not' ('not' ((Ex (c,a,G)) . PA))) '&' ('not' ((Ex (('not' b),a,G)) . PA)) is set

'not' (('not' ('not' ((Ex (c,a,G)) . PA))) '&' ('not' ((Ex (('not' b),a,G)) . PA))) is boolean set

((Ex (('not' b),a,G)) . PA) => ((Ex (c,a,G)) . PA) is set

('not' ((Ex (('not' b),a,G)) . PA)) 'or' ((Ex (c,a,G)) . PA) is set

'not' ('not' ((Ex (('not' b),a,G)) . PA)) is boolean set

('not' ('not' ((Ex (('not' b),a,G)) . PA))) '&' ('not' ((Ex (c,a,G)) . PA)) is set

'not' (('not' ('not' ((Ex (('not' b),a,G)) . PA))) '&' ('not' ((Ex (c,a,G)) . PA))) is boolean set

(((Ex (c,a,G)) . PA) => ((Ex (('not' b),a,G)) . PA)) '&' (((Ex (('not' b),a,G)) . PA) => ((Ex (c,a,G)) . PA)) is set

'not' (((Ex (c,a,G)) . PA) <=> ((Ex (('not' b),a,G)) . PA)) is boolean set

('not' ((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G)))) . PA is boolean Element of BOOLEAN

(('not' ((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G)))) . PA) 'or' (('not' ((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G)))) . PA) is set

'not' (('not' ((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G)))) . PA) is boolean set

'not' (('not' ((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G)))) . PA) is boolean set

('not' (('not' ((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G)))) . PA)) '&' ('not' (('not' ((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G)))) . PA)) is set

'not' (('not' (('not' ((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G)))) . PA)) '&' ('not' (('not' ((Ex (c,a,G)) 'xor' (Ex (('not' b),a,G)))) . PA))) is boolean set

((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G))) . PA is boolean Element of BOOLEAN

'not' (((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G))) . PA) is boolean Element of BOOLEAN

'not' FALSE is boolean Element of BOOLEAN

('not' (((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G))) . PA)) 'or' ('not' FALSE) is set

'not' ('not' (((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G))) . PA)) is boolean set

'not' ('not' FALSE) is boolean set

('not' ('not' (((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G))) . PA))) '&' ('not' ('not' FALSE)) is set

'not' (('not' ('not' (((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G))) . PA))) '&' ('not' ('not' FALSE))) is boolean set

('not' (((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G))) . PA)) 'or' TRUE is set

'not' TRUE is boolean set

('not' ('not' (((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G))) . PA))) '&' ('not' TRUE) is set

'not' (('not' ('not' (((Ex (('not' c),a,G)) 'xor' (Ex (b,a,G))) . PA))) '&' ('not' TRUE)) is boolean set

Y is non empty set

PARTITIONS Y is partition-membered Element of K10(K10(K32(Y)))

K32(Y) is Element of K10(K10(Y))

K10(Y) is set

K10(K10(Y)) is set

K10(K32(Y)) is set

K10(K10(K32(Y))) is set

K10((PARTITIONS Y)) is set

K11(Y,BOOLEAN) is set

K10(K11(Y,BOOLEAN)) is set

G is Element of K10((PARTITIONS Y))

c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

c 'or' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

a is a_partition of Y

All ((c 'or' b),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

All (c,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex (b,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(All (c,a,G)) 'or' (Ex (b,a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

PA is Element of Y

(All ((c 'or' b),a,G)) . PA is boolean Element of BOOLEAN

((All (c,a,G)) 'or' (Ex (b,a,G))) . PA is boolean Element of BOOLEAN

CompF (a,G) is a_partition of Y

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

B_INF ((c 'or' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_INF ((c 'or' b),(CompF (a,G)))) . PA is boolean Element of BOOLEAN

z is Element of Y

(c 'or' b) . z is boolean Element of BOOLEAN

B_SUP (b,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_SUP (b,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

z is Element of Y

b . z is boolean Element of BOOLEAN

(Ex (b,a,G)) . PA is boolean Element of BOOLEAN

(All (c,a,G)) . PA is boolean Element of BOOLEAN

((All (c,a,G)) . PA) 'or' TRUE is set

'not' ((All (c,a,G)) . PA) is boolean set

'not' TRUE is boolean set

('not' ((All (c,a,G)) . PA)) '&' ('not' TRUE) is set

'not' (('not' ((All (c,a,G)) . PA)) '&' ('not' TRUE)) is boolean set

B_INF (c,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_INF (c,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

(All (c,a,G)) . PA is boolean Element of BOOLEAN

(Ex (b,a,G)) . PA is boolean Element of BOOLEAN

TRUE 'or' ((Ex (b,a,G)) . PA) is set

'not' TRUE is boolean set

'not' ((Ex (b,a,G)) . PA) is boolean set

('not' TRUE) '&' ('not' ((Ex (b,a,G)) . PA)) is set

'not' (('not' TRUE) '&' ('not' ((Ex (b,a,G)) . PA))) is boolean set

z is Element of Y

c . z is boolean Element of BOOLEAN

z is Element of Y

c . z is boolean Element of BOOLEAN

b . z is boolean Element of BOOLEAN

x1 is Element of Y

c . x1 is boolean Element of BOOLEAN

(c 'or' b) . z is boolean Element of BOOLEAN

(c . z) 'or' (b . z) is set

'not' (c . z) is boolean set

'not' (b . z) is boolean set

('not' (c . z)) '&' ('not' (b . z)) is set

'not' (('not' (c . z)) '&' ('not' (b . z))) is boolean set

FALSE 'or' FALSE is set

'not' FALSE is boolean set

('not' FALSE) '&' ('not' FALSE) is set

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

z is Element of Y

c . z is boolean Element of BOOLEAN

x1 is Element of Y

b . x1 is boolean Element of BOOLEAN

c

b . c

Y is non empty set

K11(Y,BOOLEAN) is set

K10(K11(Y,BOOLEAN)) is set

PARTITIONS Y is partition-membered Element of K10(K10(K32(Y)))

K32(Y) is Element of K10(K10(Y))

K10(Y) is set

K10(K10(Y)) is set

K10(K32(Y)) is set

K10(K10(K32(Y))) is set

K10((PARTITIONS Y)) is set

G is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

G 'or' c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

b is Element of K10((PARTITIONS Y))

a is a_partition of Y

All ((G 'or' c),a,b) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

PA is Element of Y

(All ((G 'or' c),a,b)) . PA is boolean Element of BOOLEAN

CompF (a,b) is a_partition of Y

EqClass (PA,(CompF (a,b))) is Element of CompF (a,b)

B_INF ((G 'or' c),(CompF (a,b))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_INF ((G 'or' c),(CompF (a,b)))) . PA is boolean Element of BOOLEAN

z is Element of Y

(G 'or' c) . z is boolean Element of BOOLEAN

Y is non empty set

PARTITIONS Y is partition-membered Element of K10(K10(K32(Y)))

K32(Y) is Element of K10(K10(Y))

K10(Y) is set

K10(K10(Y)) is set

K10(K32(Y)) is set

K10(K10(K32(Y))) is set

K10((PARTITIONS Y)) is set

K11(Y,BOOLEAN) is set

K10(K11(Y,BOOLEAN)) is set

G is Element of K10((PARTITIONS Y))

c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

c 'or' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

a is a_partition of Y

All ((c 'or' b),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex (c,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

All (b,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(Ex (c,a,G)) 'or' (All (b,a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

PA is Element of Y

(All ((c 'or' b),a,G)) . PA is boolean Element of BOOLEAN

((Ex (c,a,G)) 'or' (All (b,a,G))) . PA is boolean Element of BOOLEAN

CompF (a,G) is a_partition of Y

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

B_SUP (c,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_SUP (c,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

z is Element of Y

c . z is boolean Element of BOOLEAN

(Ex (c,a,G)) . PA is boolean Element of BOOLEAN

(All (b,a,G)) . PA is boolean Element of BOOLEAN

TRUE 'or' ((All (b,a,G)) . PA) is set

'not' TRUE is boolean set

'not' ((All (b,a,G)) . PA) is boolean set

('not' TRUE) '&' ('not' ((All (b,a,G)) . PA)) is set

'not' (('not' TRUE) '&' ('not' ((All (b,a,G)) . PA))) is boolean set

CompF (a,G) is a_partition of Y

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

B_INF (b,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_INF (b,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

(All (b,a,G)) . PA is boolean Element of BOOLEAN

(Ex (c,a,G)) . PA is boolean Element of BOOLEAN

((Ex (c,a,G)) . PA) 'or' TRUE is set

'not' ((Ex (c,a,G)) . PA) is boolean set

'not' TRUE is boolean set

('not' ((Ex (c,a,G)) . PA)) '&' ('not' TRUE) is set

'not' (('not' ((Ex (c,a,G)) . PA)) '&' ('not' TRUE)) is boolean set

CompF (a,G) is a_partition of Y

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

z is Element of Y

b . z is boolean Element of BOOLEAN

z is Element of Y

b . z is boolean Element of BOOLEAN

c . z is boolean Element of BOOLEAN

x1 is Element of Y

b . x1 is boolean Element of BOOLEAN

(c 'or' b) . z is boolean Element of BOOLEAN

(c . z) 'or' (b . z) is set

'not' (c . z) is boolean set

'not' (b . z) is boolean set

('not' (c . z)) '&' ('not' (b . z)) is set

'not' (('not' (c . z)) '&' ('not' (b . z))) is boolean set

FALSE 'or' FALSE is set

'not' FALSE is boolean set

('not' FALSE) '&' ('not' FALSE) is set

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

CompF (a,G) is a_partition of Y

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

z is Element of Y

b . z is boolean Element of BOOLEAN

x1 is Element of Y

c . x1 is boolean Element of BOOLEAN

c

c . c

Y is non empty set

PARTITIONS Y is partition-membered Element of K10(K10(K32(Y)))

K32(Y) is Element of K10(K10(Y))

K10(Y) is set

K10(K10(Y)) is set

K10(K32(Y)) is set

K10(K10(K32(Y))) is set

K10((PARTITIONS Y)) is set

K11(Y,BOOLEAN) is set

K10(K11(Y,BOOLEAN)) is set

G is Element of K10((PARTITIONS Y))

c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

c 'or' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

a is a_partition of Y

All ((c 'or' b),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex (c,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex (b,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(Ex (c,a,G)) 'or' (Ex (b,a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

PA is Element of Y

(All ((c 'or' b),a,G)) . PA is boolean Element of BOOLEAN

((Ex (c,a,G)) 'or' (Ex (b,a,G))) . PA is boolean Element of BOOLEAN

CompF (a,G) is a_partition of Y

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

(c 'or' b) . PA is boolean Element of BOOLEAN

c . PA is boolean Element of BOOLEAN

b . PA is boolean Element of BOOLEAN

(c . PA) 'or' (b . PA) is set

'not' (c . PA) is boolean set

'not' (b . PA) is boolean set

('not' (c . PA)) '&' ('not' (b . PA)) is set

'not' (('not' (c . PA)) '&' ('not' (b . PA))) is boolean set

B_SUP (c,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_SUP (c,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

(Ex (c,a,G)) . PA is boolean Element of BOOLEAN

(Ex (b,a,G)) . PA is boolean Element of BOOLEAN

TRUE 'or' ((Ex (b,a,G)) . PA) is set

'not' TRUE is boolean set

'not' ((Ex (b,a,G)) . PA) is boolean set

('not' TRUE) '&' ('not' ((Ex (b,a,G)) . PA)) is set

'not' (('not' TRUE) '&' ('not' ((Ex (b,a,G)) . PA))) is boolean set

B_SUP (b,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_SUP (b,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

(Ex (b,a,G)) . PA is boolean Element of BOOLEAN

(Ex (c,a,G)) . PA is boolean Element of BOOLEAN

((Ex (c,a,G)) . PA) 'or' TRUE is set

'not' ((Ex (c,a,G)) . PA) is boolean set

'not' TRUE is boolean set

('not' ((Ex (c,a,G)) . PA)) '&' ('not' TRUE) is set

'not' (('not' ((Ex (c,a,G)) . PA)) '&' ('not' TRUE)) is boolean set

Y is non empty set

PARTITIONS Y is partition-membered Element of K10(K10(K32(Y)))

K32(Y) is Element of K10(K10(Y))

K10(Y) is set

K10(K10(Y)) is set

K10(K32(Y)) is set

K10(K10(K32(Y))) is set

K10((PARTITIONS Y)) is set

K11(Y,BOOLEAN) is set

K10(K11(Y,BOOLEAN)) is set

G is Element of K10((PARTITIONS Y))

c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

c '&' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

a is a_partition of Y

Ex (c,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

All (b,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(Ex (c,a,G)) '&' (All (b,a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex ((c '&' b),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

PA is Element of Y

((Ex (c,a,G)) '&' (All (b,a,G))) . PA is boolean Element of BOOLEAN

(Ex ((c '&' b),a,G)) . PA is boolean Element of BOOLEAN

(Ex (c,a,G)) . PA is boolean Element of BOOLEAN

(All (b,a,G)) . PA is boolean Element of BOOLEAN

((Ex (c,a,G)) . PA) '&' ((All (b,a,G)) . PA) is boolean Element of BOOLEAN

CompF (a,G) is a_partition of Y

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

B_INF (b,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_INF (b,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

z is Element of Y

b . z is boolean Element of BOOLEAN

B_SUP (c,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_SUP (c,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

z is Element of Y

c . z is boolean Element of BOOLEAN

z is Element of Y

c . z is boolean Element of BOOLEAN

(c '&' b) . z is boolean Element of BOOLEAN

b . z is boolean Element of BOOLEAN

(c . z) '&' (b . z) is boolean Element of BOOLEAN

TRUE '&' TRUE is boolean Element of BOOLEAN

B_SUP ((c '&' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_SUP ((c '&' b),(CompF (a,G)))) . PA is boolean Element of BOOLEAN

Y is non empty set

PARTITIONS Y is partition-membered Element of K10(K10(K32(Y)))

K32(Y) is Element of K10(K10(Y))

K10(Y) is set

K10(K10(Y)) is set

K10(K32(Y)) is set

K10(K10(K32(Y))) is set

K10((PARTITIONS Y)) is set

K11(Y,BOOLEAN) is set

K10(K11(Y,BOOLEAN)) is set

G is Element of K10((PARTITIONS Y))

c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

c '&' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

a is a_partition of Y

All (c,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex (b,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(All (c,a,G)) '&' (Ex (b,a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex ((c '&' b),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

PA is Element of Y

((All (c,a,G)) '&' (Ex (b,a,G))) . PA is boolean Element of BOOLEAN

(Ex ((c '&' b),a,G)) . PA is boolean Element of BOOLEAN

(All (c,a,G)) . PA is boolean Element of BOOLEAN

(Ex (b,a,G)) . PA is boolean Element of BOOLEAN

((All (c,a,G)) . PA) '&' ((Ex (b,a,G)) . PA) is boolean Element of BOOLEAN

CompF (a,G) is a_partition of Y

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

B_INF (c,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_INF (c,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

z is Element of Y

c . z is boolean Element of BOOLEAN

B_SUP (b,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_SUP (b,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

z is Element of Y

b . z is boolean Element of BOOLEAN

z is Element of Y

b . z is boolean Element of BOOLEAN

(c '&' b) . z is boolean Element of BOOLEAN

c . z is boolean Element of BOOLEAN

(c . z) '&' (b . z) is boolean Element of BOOLEAN

TRUE '&' TRUE is boolean Element of BOOLEAN

B_SUP ((c '&' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_SUP ((c '&' b),(CompF (a,G)))) . PA is boolean Element of BOOLEAN

Y is non empty set

K11(Y,BOOLEAN) is set

K10(K11(Y,BOOLEAN)) is set

PARTITIONS Y is partition-membered Element of K10(K10(K32(Y)))

K32(Y) is Element of K10(K10(Y))

K10(Y) is set

K10(K10(Y)) is set

K10(K32(Y)) is set

K10(K10(K32(Y))) is set

K10((PARTITIONS Y)) is set

G is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

G 'imp' c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

b is Element of K10((PARTITIONS Y))

a is a_partition of Y

All ((G 'imp' c),a,b) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

PA is Element of Y

(All ((G 'imp' c),a,b)) . PA is boolean Element of BOOLEAN

CompF (a,b) is a_partition of Y

EqClass (PA,(CompF (a,b))) is Element of CompF (a,b)

B_INF ((G 'imp' c),(CompF (a,b))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_INF ((G 'imp' c),(CompF (a,b)))) . PA is boolean Element of BOOLEAN

z is Element of Y

(G 'imp' c) . z is boolean Element of BOOLEAN

Y is non empty set

PARTITIONS Y is partition-membered Element of K10(K10(K32(Y)))

K32(Y) is Element of K10(K10(Y))

K10(Y) is set

K10(K10(Y)) is set

K10(K32(Y)) is set

K10(K10(K32(Y))) is set

K10((PARTITIONS Y)) is set

K11(Y,BOOLEAN) is set

K10(K11(Y,BOOLEAN)) is set

G is Element of K10((PARTITIONS Y))

c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

c 'imp' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

a is a_partition of Y

All ((c 'imp' b),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

All (c,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex (b,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(All (c,a,G)) 'imp' (Ex (b,a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

CompF (a,G) is a_partition of Y

B_INF (c,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

PA is Element of Y

(All ((c 'imp' b),a,G)) . PA is boolean Element of BOOLEAN

((All (c,a,G)) 'imp' (Ex (b,a,G))) . PA is boolean Element of BOOLEAN

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

B_SUP (b,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_SUP (b,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

z is Element of Y

b . z is boolean Element of BOOLEAN

(Ex (b,a,G)) . PA is boolean Element of BOOLEAN

(All (c,a,G)) . PA is boolean Element of BOOLEAN

'not' ((All (c,a,G)) . PA) is boolean Element of BOOLEAN

('not' ((All (c,a,G)) . PA)) 'or' TRUE is set

'not' ('not' ((All (c,a,G)) . PA)) is boolean set

'not' TRUE is boolean set

('not' ('not' ((All (c,a,G)) . PA))) '&' ('not' TRUE) is set

'not' (('not' ('not' ((All (c,a,G)) . PA))) '&' ('not' TRUE)) is boolean set

b . PA is boolean Element of BOOLEAN

c . PA is boolean Element of BOOLEAN

(c 'imp' b) . PA is boolean Element of BOOLEAN

'not' (c . PA) is boolean Element of BOOLEAN

('not' (c . PA)) 'or' (b . PA) is set

'not' ('not' (c . PA)) is boolean set

'not' (b . PA) is boolean set

('not' ('not' (c . PA))) '&' ('not' (b . PA)) is set

'not' (('not' ('not' (c . PA))) '&' ('not' (b . PA))) is boolean set

'not' TRUE is boolean Element of BOOLEAN

('not' TRUE) 'or' FALSE is set

'not' ('not' TRUE) is boolean set

'not' FALSE is boolean set

('not' ('not' TRUE)) '&' ('not' FALSE) is set

'not' (('not' ('not' TRUE)) '&' ('not' FALSE)) is boolean set

FALSE 'or' FALSE is set

('not' FALSE) '&' ('not' FALSE) is set

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

(All (c,a,G)) . PA is boolean Element of BOOLEAN

'not' ((All (c,a,G)) . PA) is boolean Element of BOOLEAN

(Ex (b,a,G)) . PA is boolean Element of BOOLEAN

('not' ((All (c,a,G)) . PA)) 'or' ((Ex (b,a,G)) . PA) is set

'not' ('not' ((All (c,a,G)) . PA)) is boolean set

'not' ((Ex (b,a,G)) . PA) is boolean set

('not' ('not' ((All (c,a,G)) . PA))) '&' ('not' ((Ex (b,a,G)) . PA)) is set

'not' (('not' ('not' ((All (c,a,G)) . PA))) '&' ('not' ((Ex (b,a,G)) . PA))) is boolean set

'not' FALSE is boolean Element of BOOLEAN

('not' FALSE) 'or' ((Ex (b,a,G)) . PA) is set

'not' ('not' FALSE) is boolean set

('not' ('not' FALSE)) '&' ('not' ((Ex (b,a,G)) . PA)) is set

'not' (('not' ('not' FALSE)) '&' ('not' ((Ex (b,a,G)) . PA))) is boolean set

TRUE 'or' ((Ex (b,a,G)) . PA) is set

'not' TRUE is boolean set

('not' TRUE) '&' ('not' ((Ex (b,a,G)) . PA)) is set

'not' (('not' TRUE) '&' ('not' ((Ex (b,a,G)) . PA))) is boolean set

z is Element of Y

c . z is boolean Element of BOOLEAN

z is Element of Y

c . z is boolean Element of BOOLEAN

x1 is Element of Y

b . x1 is boolean Element of BOOLEAN

c

b . c

Y is non empty set

PARTITIONS Y is partition-membered Element of K10(K10(K32(Y)))

K32(Y) is Element of K10(K10(Y))

K10(Y) is set

K10(K10(Y)) is set

K10(K32(Y)) is set

K10(K10(K32(Y))) is set

K10((PARTITIONS Y)) is set

K11(Y,BOOLEAN) is set

K10(K11(Y,BOOLEAN)) is set

G is Element of K10((PARTITIONS Y))

c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

c 'imp' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

a is a_partition of Y

All ((c 'imp' b),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex (c,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

Ex (b,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(Ex (c,a,G)) 'imp' (Ex (b,a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

CompF (a,G) is a_partition of Y

B_SUP (c,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

PA is Element of Y

(All ((c 'imp' b),a,G)) . PA is boolean Element of BOOLEAN

((Ex (c,a,G)) 'imp' (Ex (b,a,G))) . PA is boolean Element of BOOLEAN

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

B_SUP (b,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(B_SUP (b,(CompF (a,G)))) . PA is boolean Element of BOOLEAN

z is Element of Y

b . z is boolean Element of BOOLEAN

(Ex (b,a,G)) . PA is boolean Element of BOOLEAN

(Ex (c,a,G)) . PA is boolean Element of BOOLEAN

'not' ((Ex (c,a,G)) . PA) is boolean Element of BOOLEAN

('not' ((Ex (c,a,G)) . PA)) 'or' TRUE is set

'not' ('not' ((Ex (c,a,G)) . PA)) is boolean set

'not' TRUE is boolean set

('not' ('not' ((Ex (c,a,G)) . PA))) '&' ('not' TRUE) is set

'not' (('not' ('not' ((Ex (c,a,G)) . PA))) '&' ('not' TRUE)) is boolean set

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)

z is Element of Y

c . z is boolean Element of BOOLEAN

z is Element of Y

c . z is boolean Element of BOOLEAN

b . z is boolean Element of BOOLEAN

x1 is Element of Y

c . x1 is boolean Element of BOOLEAN

(c 'imp' b) . z is boolean Element of BOOLEAN

'not' (c . z) is boolean Element of BOOLEAN

('not' (c . z)) 'or' (b . z) is set

'not' ('not' (c . z)) is boolean set

'not' (b . z) is boolean set

('not' ('not' (c . z))) '&' ('not' (b . z)) is set

'not' (('not' ('not' (c . z)