:: 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₉ is Element of Y
b . c₉ 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 '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₉ is Element of Y
c . c₉ 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))
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₉ is Element of Y
b . c₉ 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))
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))) '&' ('not' (b . z))) 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
EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)
(Ex (c,a,G)) . PA is boolean Element of BOOLEAN
'not' ((Ex (c,a,G)) . PA) is boolean Element of BOOLEAN
(Ex (b,a,G)) . PA is boolean Element of BOOLEAN
('not' ((Ex (c,a,G)) . PA)) 'or' ((Ex (b,a,G)) . PA) is set
'not' ('not' ((Ex (c,a,G)) . PA)) is boolean set
'not' ((Ex (b,a,G)) . PA) is boolean set
('not' ('not' ((Ex (c,a,G)) . PA))) '&' ('not' ((Ex (b,a,G)) . PA)) is set
'not' (('not' ('not' ((Ex (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
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₉ is Element of Y
b . c₉ 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
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)) 'imp' (All (b,a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
All ((c 'imp' b),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
PA is Element of Y
((Ex (c,a,G)) 'imp' (All (b,a,G))) . PA is boolean Element of BOOLEAN
(All ((c 'imp' 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
(All (b,a,G)) . PA is boolean Element of BOOLEAN
('not' ((Ex (c,a,G)) . PA)) 'or' ((All (b,a,G)) . PA) is set
'not' ('not' ((Ex (c,a,G)) . PA)) is boolean set
'not' ((All (b,a,G)) . PA) is boolean set
('not' ('not' ((Ex (c,a,G)) . PA))) '&' ('not' ((All (b,a,G)) . PA)) is set
'not' (('not' ('not' ((Ex (c,a,G)) . PA))) '&' ('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)
z is Element of Y
(c 'imp' b) . z is boolean Element of BOOLEAN
c . z is boolean Element of BOOLEAN
'not' (c . z) is boolean Element of BOOLEAN
b . 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))) '&' ('not' (b . z))) is boolean set
('not' (c . z)) 'or' TRUE is set
'not' TRUE is boolean set
('not' ('not' (c . z))) '&' ('not' TRUE) is set
'not' (('not' ('not' (c . z))) '&' ('not' TRUE)) is boolean set
B_INF ((c 'imp' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' b),(CompF (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
x1 is Element of Y
b . x1 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
c . z is boolean Element of BOOLEAN
x1 is Element of Y
b . x1 is boolean Element of BOOLEAN
CompF (a,G) is a_partition of Y
EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)
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 'imp' b) . z is boolean Element of BOOLEAN
'not' (c . z) is boolean Element of BOOLEAN
b . 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))) '&' ('not' (b . z))) is boolean set
'not' FALSE is boolean Element of BOOLEAN
('not' FALSE) 'or' (b . z) is set
'not' ('not' FALSE) is boolean set
('not' ('not' FALSE)) '&' ('not' (b . z)) is set
'not' (('not' ('not' FALSE)) '&' ('not' (b . z))) is boolean set
TRUE 'or' (b . z) is set
'not' TRUE is boolean set
('not' TRUE) '&' ('not' (b . z)) is set
'not' (('not' TRUE) '&' ('not' (b . z))) is boolean set
B_INF ((c 'imp' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' b),(CompF (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)
z is Element of Y
b . z is boolean Element of BOOLEAN
x1 is Element of Y
c . x1 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
Ex (b,a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c '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
(c '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
(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
('not' (c . PA)) 'or' TRUE is set
'not' TRUE is boolean set
('not' ('not' (c . PA))) '&' ('not' TRUE) is set
'not' (('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 '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))
(All (c,a,G)) 'imp' b 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' b) . 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
('not' FALSE) 'or' (b . PA) is set
'not' ('not' FALSE) is boolean set
('not' ('not' FALSE)) '&' ('not' (b . PA)) is set
'not' (('not' ('not' FALSE)) '&' ('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
(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 'imp' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a is a_partition of Y
Ex ((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))
PA is Element of Y
(Ex ((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
CompF (a,G) is a_partition of Y
EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)
B_SUP ((c 'imp' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((c 'imp' b),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
z is Element of Y
(c 'imp' b) . z is boolean Element of BOOLEAN
z is Element of Y
(c 'imp' b) . z is boolean Element of BOOLEAN
c . z is boolean Element of BOOLEAN
'not' (c . z) is boolean Element of BOOLEAN
b . 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))) '&' ('not' (b . z))) 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))
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))
(Ex (b,a,G)) 'imp' (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)) . PA is boolean Element of BOOLEAN
((Ex (b,a,G)) 'imp' (Ex ((c '&' 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
(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))
(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
(Ex ((c '&' b),a,G)) . PA is boolean Element of BOOLEAN
'not' ((Ex (b,a,G)) . PA) is boolean Element of BOOLEAN
('not' ((Ex (b,a,G)) . PA)) 'or' TRUE is set
'not' ('not' ((Ex (b,a,G)) . PA)) is boolean set
'not' TRUE is boolean set
('not' ('not' ((Ex (b,a,G)) . PA))) '&' ('not' TRUE) is set
'not' (('not' ('not' ((Ex (b,a,G)) . PA))) '&' ('not' TRUE)) is boolean set
(Ex (b,a,G)) . PA is boolean Element of BOOLEAN
'not' FALSE is boolean Element of BOOLEAN
(Ex ((c '&' b),a,G)) . PA is boolean Element of BOOLEAN
('not' FALSE) 'or' ((Ex ((c '&' b),a,G)) . PA) is set
'not' ('not' FALSE) is boolean set
'not' ((Ex ((c '&' b),a,G)) . PA) is boolean set
('not' ('not' FALSE)) '&' ('not' ((Ex ((c '&' b),a,G)) . PA)) is set
'not' (('not' ('not' FALSE)) '&' ('not' ((Ex ((c '&' b),a,G)) . PA))) is boolean set
TRUE 'or' ((Ex ((c '&' b),a,G)) . PA) is set
'not' TRUE is boolean set
('not' TRUE) '&' ('not' ((Ex ((c '&' b),a,G)) . PA)) is set
'not' (('not' TRUE) '&' ('not' ((Ex ((c '&' b),a,G)) . PA))) is boolean set
(Ex (b,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 'imp' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a is a_partition of Y
Ex ((c 'imp' b),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))
c '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
PA is Element of Y
(Ex ((c 'imp' b),a,G)) . PA is boolean Element of BOOLEAN
(c 'imp' (Ex (b,a,G))) . PA is boolean Element of BOOLEAN
EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)
B_SUP ((c 'imp' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((c 'imp' b),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
z is Element of Y
(c 'imp' b) . z is boolean Element of BOOLEAN
z is Element of Y
(c 'imp' b) . z is boolean Element of BOOLEAN
c . z is boolean Element of BOOLEAN
'not' (c . z) is boolean Element of BOOLEAN
b . 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))) '&' ('not' (b . z))) is boolean set
c . 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
c . PA is boolean Element of BOOLEAN
'not' (c . PA) is boolean Element of BOOLEAN
('not' (c . PA)) 'or' TRUE is set
'not' ('not' (c . PA)) is boolean set
'not' TRUE is boolean set
('not' ('not' (c . PA))) '&' ('not' TRUE) is set
'not' (('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))
b 'imp' c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a is a_partition of Y
Ex ((b 'imp' 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 (b,a,G)) 'imp' c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
CompF (a,G) is a_partition of Y
PA is Element of Y
(Ex ((b 'imp' c),a,G)) . PA is boolean Element of BOOLEAN
((All (b,a,G)) 'imp' c) . PA is boolean Element of BOOLEAN
EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)
B_SUP ((b 'imp' c),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((b 'imp' c),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
z is Element of Y
(b 'imp' c) . z is boolean Element of BOOLEAN
z is Element of Y
(b 'imp' c) . z is boolean Element of BOOLEAN
b . z is boolean Element of BOOLEAN
'not' (b . z) is boolean Element of BOOLEAN
c . z is boolean Element of BOOLEAN
('not' (b . z)) 'or' (c . z) is set
'not' ('not' (b . z)) is boolean set
'not' (c . z) is boolean set
('not' ('not' (b . z))) '&' ('not' (c . z)) is set
'not' (('not' ('not' (b . z))) '&' ('not' (c . z))) 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
(All (b,a,G)) . PA is boolean Element of BOOLEAN
'not' FALSE is boolean Element of BOOLEAN
c . PA is boolean Element of BOOLEAN
('not' FALSE) 'or' (c . PA) is set
'not' ('not' FALSE) is boolean set
'not' (c . PA) is boolean set
('not' ('not' FALSE)) '&' ('not' (c . PA)) is set
'not' (('not' ('not' FALSE)) '&' ('not' (c . PA))) is boolean set
TRUE 'or' (c . PA) is set
'not' TRUE is boolean set
('not' TRUE) '&' ('not' (c . PA)) is set
'not' (('not' TRUE) '&' ('not' (c . PA))) is boolean set
c . PA is boolean Element of BOOLEAN
(All (b,a,G)) . PA is boolean Element of BOOLEAN
'not' ((All (b,a,G)) . PA) is boolean Element of BOOLEAN
('not' ((All (b,a,G)) . PA)) 'or' TRUE is set
'not' ('not' ((All (b,a,G)) . PA)) is boolean set
'not' TRUE is boolean set
('not' ('not' ((All (b,a,G)) . PA))) '&' ('not' TRUE) is set
'not' (('not' ('not' ((All (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 '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))
Ex ((c 'imp' 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,a,G)) 'imp' (Ex (b,a,G))) . PA is boolean Element of BOOLEAN
(Ex ((c 'imp' 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
(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
EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)
z is Element of Y
c . z is boolean Element of BOOLEAN
(c 'imp' b) . z is boolean Element of BOOLEAN
'not' (c . z) is boolean Element of BOOLEAN
b . 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))) '&' ('not' (b . z))) is boolean set
'not' FALSE is boolean Element of BOOLEAN
('not' FALSE) 'or' (b . z) is set
'not' ('not' FALSE) is boolean set
('not' ('not' FALSE)) '&' ('not' (b . z)) is set
'not' (('not' ('not' FALSE)) '&' ('not' (b . z))) is boolean set
TRUE 'or' (b . z) is set
'not' TRUE is boolean set
('not' TRUE) '&' ('not' (b . z)) is set
'not' (('not' TRUE) '&' ('not' (b . z))) is boolean set
B_SUP ((c 'imp' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((c 'imp' b),(CompF (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
z is Element of Y
b . z is boolean Element of BOOLEAN
(c 'imp' b) . z is boolean Element of BOOLEAN
c . z is boolean Element of BOOLEAN
'not' (c . z) is boolean Element of BOOLEAN
('not' (c . z)) 'or' TRUE is set
'not' ('not' (c . z)) is boolean set
'not' TRUE is boolean set
('not' ('not' (c . z))) '&' ('not' TRUE) is set
'not' (('not' ('not' (c . z))) '&' ('not' TRUE)) is boolean set
B_SUP ((c 'imp' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((c 'imp' b),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
PA is Element of Y
(Ex ((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 ((c 'imp' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((c 'imp' b),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
z is Element of Y
(c 'imp' b) . z is boolean Element of BOOLEAN
z is Element of Y
(c 'imp' b) . z is boolean Element of BOOLEAN
c . z is boolean Element of BOOLEAN
'not' (c . z) is boolean Element of BOOLEAN
b . 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))) '&' ('not' (b . z))) is boolean set
(B_INF (c,(CompF (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))
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)) 'imp' (All (b,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
((All (c,a,G)) 'imp' (All (b,a,G))) . PA is boolean Element of BOOLEAN
((All (c,a,G)) 'imp' (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
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
('not' ((All (c,a,G)) . PA)) 'or' ((All (b,a,G)) . PA) is set
'not' ('not' ((All (c,a,G)) . PA)) is boolean set
'not' ((All (b,a,G)) . PA) is boolean set
('not' ('not' ((All (c,a,G)) . PA))) '&' ('not' ((All (b,a,G)) . PA)) is set
'not' (('not' ('not' ((All (c,a,G)) . PA))) '&' ('not' ((All (b,a,G)) . PA))) is boolean set
(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_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
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
('not' ((All (c,a,G)) . PA)) 'or' TRUE is 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))
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)) 'imp' (Ex (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))
(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_SUP (c,(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
PA is Element of Y
((Ex (c,a,G)) 'imp' (Ex (b,a,G))) . PA is boolean Element of BOOLEAN
((All (c,a,G)) 'imp' (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
(Ex (b,a,G)) . PA is boolean Element of BOOLEAN
('not' ((Ex (c,a,G)) . PA)) 'or' ((Ex (b,a,G)) . PA) is set
'not' ('not' ((Ex (c,a,G)) . PA)) is boolean set
'not' ((Ex (b,a,G)) . PA) is boolean set
('not' ('not' ((Ex (c,a,G)) . PA))) '&' ('not' ((Ex (b,a,G)) . PA)) is set
'not' (('not' ('not' ((Ex (c,a,G)) . PA))) '&' ('not' ((Ex (b,a,G)) . PA))) is boolean set
EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)
c . PA is boolean Element of BOOLEAN
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
('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
(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))
'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 'imp' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' c) 'or' 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 ((('not' c) 'or' b),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
PA is Element of Y
(All ((('not' c) 'or' b),a,G)) . PA is boolean Element of BOOLEAN
(All ((c 'imp' 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 ((('not' c) 'or' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((('not' c) 'or' b),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
z is Element of Y
(('not' c) 'or' b) . z is boolean Element of BOOLEAN
z is Element of Y
(c 'imp' b) . z is boolean Element of BOOLEAN
('not' c) . z is boolean Element of BOOLEAN
(('not' c) 'or' b) . z is boolean Element of BOOLEAN
b . 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)) '&' ('not' (b . z))) is boolean set
c . z is boolean Element of BOOLEAN
'not' (c . z) is boolean Element of BOOLEAN
TRUE 'or' (b . z) is set
'not' TRUE is boolean set
('not' TRUE) '&' ('not' (b . z)) is set
'not' (('not' TRUE) '&' ('not' (b . z))) is boolean set
c . z is boolean Element of BOOLEAN
'not' (c . z) is boolean Element of BOOLEAN
('not' (c . z)) 'or' TRUE is set
'not' ('not' (c . z)) is boolean set
'not' TRUE is boolean set
('not' ('not' (c . z))) '&' ('not' TRUE) is set
'not' (('not' ('not' (c . z))) '&' ('not' TRUE)) is boolean set
B_INF ((c 'imp' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' b),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
PA is Element of Y
(All ((c 'imp' b),a,G)) . PA is boolean Element of BOOLEAN
(All ((('not' c) 'or' 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 'imp' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' b),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
z is Element of Y
(c 'imp' b) . z is boolean Element of BOOLEAN
z is Element of Y
c . z is boolean Element of BOOLEAN
'not' (c . z) is boolean Element of BOOLEAN
(c 'imp' b) . z is boolean Element of BOOLEAN
b . 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))) '&' ('not' (b . z))) is boolean set
('not' c) . z is boolean Element of BOOLEAN
(('not' c) 'or' b) . z is boolean Element of BOOLEAN
TRUE 'or' (b . z) is set
'not' TRUE is boolean set
('not' TRUE) '&' ('not' (b . z)) is set
'not' (('not' TRUE) '&' ('not' (b . z))) is boolean set
(('not' c) 'or' b) . z is boolean Element of BOOLEAN
('not' c) . z is boolean Element of BOOLEAN
(('not' c) . z) 'or' TRUE is set
'not' (('not' c) . z) is boolean set
'not' TRUE is boolean set
('not' (('not' c) . z)) '&' ('not' TRUE) is set
'not' (('not' (('not' c) . z)) '&' ('not' TRUE)) is boolean set
B_INF ((('not' c) 'or' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((('not' c) 'or' 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 'imp' 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))
c '&' ('not' 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 '&' ('not' b)),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (Ex ((c '&' ('not' b)),a,G)) 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))
('not' c) 'or' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
All ((('not' c) 'or' b),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (All ((('not' c) 'or' b),a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (('not' c) 'or' b) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Ex (('not' (('not' c) 'or' b)),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ('not' c) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' ('not' c)) '&' ('not' b) is V12() quasi_total boolean-valued Element of K10(K11(Y,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))
'not' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c 'imp' ('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))
All ((c 'imp' b),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
All ((c 'imp' ('not' b)),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(All ((c 'imp' b),a,G)) '&' (All ((c 'imp' ('not' b)),a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ((All ((c 'imp' b),a,G)) '&' (All ((c 'imp' ('not' b)),a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
PA is Element of Y
(Ex (c,a,G)) . PA is boolean Element of BOOLEAN
('not' ((All ((c 'imp' b),a,G)) '&' (All ((c 'imp' ('not' b)),a,G)))) . PA is boolean Element of BOOLEAN
((All ((c 'imp' b),a,G)) '&' (All ((c 'imp' ('not' b)),a,G))) . PA is boolean Element of BOOLEAN
'not' (((All ((c 'imp' b),a,G)) '&' (All ((c 'imp' ('not' b)),a,G))) . PA) is boolean Element of BOOLEAN
(All ((c 'imp' b),a,G)) . PA is boolean Element of BOOLEAN
(All ((c 'imp' ('not' b)),a,G)) . PA is boolean Element of BOOLEAN
((All ((c 'imp' b),a,G)) . PA) '&' ((All ((c 'imp' ('not' b)),a,G)) . PA) is boolean Element of BOOLEAN
'not' (((All ((c 'imp' b),a,G)) . PA) '&' ((All ((c 'imp' ('not' 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
z is Element of Y
c . z is boolean Element of BOOLEAN
(c 'imp' b) . z is boolean Element of BOOLEAN
'not' TRUE is boolean Element of BOOLEAN
b . z is boolean Element of BOOLEAN
('not' TRUE) 'or' (b . z) is set
'not' ('not' TRUE) is boolean set
'not' (b . z) is boolean set
('not' ('not' TRUE)) '&' ('not' (b . z)) is set
'not' (('not' ('not' TRUE)) '&' ('not' (b . z))) is boolean set
FALSE 'or' (b . z) is set
'not' FALSE is boolean set
('not' FALSE) '&' ('not' (b . z)) is set
'not' (('not' FALSE) '&' ('not' (b . z))) is boolean set
(c 'imp' ('not' b)) . z is boolean Element of BOOLEAN
('not' b) . z is boolean Element of BOOLEAN
('not' TRUE) 'or' (('not' b) . z) is set
'not' (('not' b) . z) is boolean set
('not' ('not' TRUE)) '&' ('not' (('not' b) . z)) is set
'not' (('not' ('not' TRUE)) '&' ('not' (('not' b) . z))) is boolean set
FALSE 'or' (('not' b) . z) is set
('not' FALSE) '&' ('not' (('not' b) . z)) is set
'not' (('not' FALSE) '&' ('not' (('not' b) . z))) is boolean set
B_INF ((c 'imp' ('not' b)),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' ('not' b)),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
((All ((c 'imp' b),a,G)) . PA) '&' FALSE is boolean Element of BOOLEAN
'not' (((All ((c 'imp' b),a,G)) . PA) '&' FALSE) is boolean Element of BOOLEAN
'not' FALSE is boolean Element of BOOLEAN
B_INF ((c 'imp' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' b),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
FALSE '&' ((All ((c 'imp' ('not' b)),a,G)) . PA) is boolean Element of BOOLEAN
'not' (FALSE '&' ((All ((c 'imp' ('not' b)),a,G)) . PA)) is boolean Element of BOOLEAN
'not' FALSE 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))
'not' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c '&' ('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 ((c '&' b),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (Ex ((c '&' b),a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Ex ((c '&' ('not' b)),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (Ex ((c '&' ('not' b)),a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' (Ex ((c '&' b),a,G))) '&' ('not' (Ex ((c '&' ('not' b)),a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (('not' (Ex ((c '&' b),a,G))) '&' ('not' (Ex ((c '&' ('not' b)),a,G)))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
PA is Element of Y
(Ex (c,a,G)) . PA is boolean Element of BOOLEAN
('not' (('not' (Ex ((c '&' b),a,G))) '&' ('not' (Ex ((c '&' ('not' b)),a,G))))) . PA is boolean Element of BOOLEAN
('not' (Ex ((c '&' ('not' b)),a,G))) . PA is boolean Element of BOOLEAN
(Ex ((c '&' ('not' b)),a,G)) . PA is boolean Element of BOOLEAN
'not' ((Ex ((c '&' ('not' b)),a,G)) . PA) is boolean Element of BOOLEAN
(('not' (Ex ((c '&' b),a,G))) '&' ('not' (Ex ((c '&' ('not' b)),a,G)))) . PA is boolean Element of BOOLEAN
'not' ((('not' (Ex ((c '&' b),a,G))) '&' ('not' (Ex ((c '&' ('not' b)),a,G)))) . PA) is boolean Element of BOOLEAN
('not' (Ex ((c '&' b),a,G))) . PA is boolean Element of BOOLEAN
(('not' (Ex ((c '&' b),a,G))) . PA) '&' (('not' (Ex ((c '&' ('not' b)),a,G))) . PA) is boolean Element of BOOLEAN
'not' ((('not' (Ex ((c '&' b),a,G))) . PA) '&' (('not' (Ex ((c '&' ('not' b)),a,G))) . PA)) is boolean Element of BOOLEAN
(Ex ((c '&' b),a,G)) . PA is boolean Element of BOOLEAN
'not' ((Ex ((c '&' b),a,G)) . PA) is boolean Element of BOOLEAN
('not' ((Ex ((c '&' b),a,G)) . PA)) '&' ('not' ((Ex ((c '&' ('not' b)),a,G)) . PA)) is boolean Element of BOOLEAN
'not' (('not' ((Ex ((c '&' b),a,G)) . PA)) '&' ('not' ((Ex ((c '&' ('not' 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
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
TRUE '&' (b . z) is boolean Element of BOOLEAN
(c '&' ('not' b)) . z is boolean Element of BOOLEAN
('not' b) . z is boolean Element of BOOLEAN
TRUE '&' (('not' b) . z) 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
'not' TRUE is boolean Element of BOOLEAN
('not' TRUE) '&' ('not' ((Ex ((c '&' ('not' b)),a,G)) . PA)) is boolean Element of BOOLEAN
'not' (('not' TRUE) '&' ('not' ((Ex ((c '&' ('not' b)),a,G)) . PA))) is boolean Element of BOOLEAN
FALSE '&' ('not' ((Ex ((c '&' ('not' b)),a,G)) . PA)) is boolean Element of BOOLEAN
'not' (FALSE '&' ('not' ((Ex ((c '&' ('not' b)),a,G)) . PA))) is boolean Element of BOOLEAN
'not' FALSE is boolean Element of BOOLEAN
'not' FALSE is boolean Element of BOOLEAN
B_SUP ((c '&' ('not' b)),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((c '&' ('not' b)),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
'not' TRUE is boolean Element of BOOLEAN
('not' ((Ex ((c '&' b),a,G)) . PA)) '&' ('not' TRUE) is boolean Element of BOOLEAN
'not' (('not' ((Ex ((c '&' b),a,G)) . PA)) '&' ('not' TRUE)) is boolean Element of BOOLEAN
('not' ((Ex ((c '&' b),a,G)) . PA)) '&' FALSE is boolean Element of BOOLEAN
'not' (('not' ((Ex ((c '&' b),a,G)) . PA)) '&' FALSE) 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))
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 ((c 'imp' b),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Ex (c,a,G)) '&' (All ((c 'imp' 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 ((c 'imp' b),a,G))) . PA is boolean Element of BOOLEAN
(Ex ((c '&' b),a,G)) . PA is boolean Element of BOOLEAN
'not' FALSE is boolean Element of BOOLEAN
(Ex (c,a,G)) . PA is boolean Element of BOOLEAN
(All ((c 'imp' b),a,G)) . PA is boolean Element of BOOLEAN
((Ex (c,a,G)) . PA) '&' ((All ((c 'imp' 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
z is Element of Y
c . z is boolean Element of BOOLEAN
B_INF ((c 'imp' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' b),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
x1 is Element of Y
(c 'imp' b) . x1 is boolean Element of BOOLEAN
(c 'imp' b) . z is boolean Element of BOOLEAN
'not' (c . z) is boolean Element of BOOLEAN
b . 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))) '&' ('not' (b . z))) is boolean set
(c '&' 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))
c 'imp' 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 ((c '&' b),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (Ex ((c '&' b),a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Ex (c,a,G)) '&' ('not' (Ex ((c '&' b),a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
All ((c 'imp' b),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (All ((c 'imp' b),a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
PA is Element of Y
((Ex (c,a,G)) '&' ('not' (Ex ((c '&' b),a,G)))) . PA is boolean Element of BOOLEAN
('not' (All ((c 'imp' b),a,G))) . PA is boolean Element of BOOLEAN
(Ex (c,a,G)) . PA is boolean Element of BOOLEAN
('not' (Ex ((c '&' b),a,G))) . PA is boolean Element of BOOLEAN
((Ex (c,a,G)) . PA) '&' (('not' (Ex ((c '&' 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
z is Element of Y
c . z is boolean Element of BOOLEAN
(Ex ((c '&' b),a,G)) . PA is boolean Element of BOOLEAN
'not' ((Ex ((c '&' b),a,G)) . PA) is boolean Element of BOOLEAN
B_SUP ((c '&' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,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
(c 'imp' b) . z is boolean Element of BOOLEAN
'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
B_INF ((c 'imp' b),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' b),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
(All ((c 'imp' b),a,G)) . PA is boolean Element of BOOLEAN
'not' FALSE 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 V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b 'imp' a is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c 'imp' a is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
PA is a_partition of Y
All ((c 'imp' b),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
All ((b 'imp' a),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(All ((c 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
All ((c 'imp' a),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
z is Element of Y
((All ((c 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))) . z is boolean Element of BOOLEAN
(All ((c 'imp' a),PA,G)) . z is boolean Element of BOOLEAN
(All ((c 'imp' b),PA,G)) . z is boolean Element of BOOLEAN
(All ((b 'imp' a),PA,G)) . z is boolean Element of BOOLEAN
((All ((c 'imp' b),PA,G)) . z) '&' ((All ((b 'imp' a),PA,G)) . z) is boolean Element of BOOLEAN
CompF (PA,G) is a_partition of Y
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
B_INF ((b 'imp' a),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((b 'imp' a),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
x1 is Element of Y
(b 'imp' a) . x1 is boolean Element of BOOLEAN
B_INF ((c 'imp' b),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' b),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
x1 is Element of Y
(c 'imp' b) . x1 is boolean Element of BOOLEAN
x1 is Element of Y
(c 'imp' a) . x1 is boolean Element of BOOLEAN
c . x1 is boolean Element of BOOLEAN
'not' (c . x1) is boolean Element of BOOLEAN
b . x1 is boolean Element of BOOLEAN
'not' (b . x1) is boolean Element of BOOLEAN
(c 'imp' b) . x1 is boolean Element of BOOLEAN
('not' (c . x1)) 'or' (b . x1) is set
'not' ('not' (c . x1)) is boolean set
'not' (b . x1) is boolean set
('not' ('not' (c . x1))) '&' ('not' (b . x1)) is set
'not' (('not' ('not' (c . x1))) '&' ('not' (b . x1))) is boolean set
(b 'imp' a) . x1 is boolean Element of BOOLEAN
a . x1 is boolean Element of BOOLEAN
('not' (b . x1)) 'or' (a . x1) is set
'not' ('not' (b . x1)) is boolean set
'not' (a . x1) is boolean set
('not' ('not' (b . x1))) '&' ('not' (a . x1)) is set
'not' (('not' ('not' (b . x1))) '&' ('not' (a . x1))) is boolean set
TRUE 'or' (a . x1) is set
'not' TRUE is boolean set
('not' TRUE) '&' ('not' (a . x1)) is set
'not' (('not' TRUE) '&' ('not' (a . x1))) is boolean set
TRUE 'or' (a . x1) is set
'not' TRUE is boolean set
('not' TRUE) '&' ('not' (a . x1)) is set
'not' (('not' TRUE) '&' ('not' (a . x1))) is boolean set
('not' (c . x1)) 'or' TRUE is set
'not' TRUE is boolean set
('not' ('not' (c . x1))) '&' ('not' TRUE) is set
'not' (('not' ('not' (c . x1))) '&' ('not' TRUE)) is boolean set
B_INF ((c 'imp' a),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' a),(CompF (PA,G)))) . 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 V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
PA is a_partition of Y
All ((c 'imp' b),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Ex ((a '&' c),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(All ((c 'imp' b),PA,G)) '&' (Ex ((a '&' c),PA,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Ex ((a '&' b),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
z is Element of Y
((All ((c 'imp' b),PA,G)) '&' (Ex ((a '&' c),PA,G))) . z is boolean Element of BOOLEAN
(Ex ((a '&' b),PA,G)) . z is boolean Element of BOOLEAN
(All ((c 'imp' b),PA,G)) . z is boolean Element of BOOLEAN
(Ex ((a '&' c),PA,G)) . z is boolean Element of BOOLEAN
((All ((c 'imp' b),PA,G)) . z) '&' ((Ex ((a '&' c),PA,G)) . z) is boolean Element of BOOLEAN
CompF (PA,G) is a_partition of Y
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
B_SUP ((a '&' c),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((a '&' c),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
x1 is Element of Y
(a '&' c) . x1 is boolean Element of BOOLEAN
x1 is Element of Y
(a '&' c) . x1 is boolean Element of BOOLEAN
a . x1 is boolean Element of BOOLEAN
c . x1 is boolean Element of BOOLEAN
(a . x1) '&' (c . x1) is boolean Element of BOOLEAN
B_INF ((c 'imp' b),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' b),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
c₉ is Element of Y
(c 'imp' b) . c₉ is boolean Element of BOOLEAN
(c 'imp' b) . x1 is boolean Element of BOOLEAN
'not' (c . x1) is boolean Element of BOOLEAN
b . x1 is boolean Element of BOOLEAN
('not' (c . x1)) 'or' (b . x1) is set
'not' ('not' (c . x1)) is boolean set
'not' (b . x1) is boolean set
('not' ('not' (c . x1))) '&' ('not' (b . x1)) is set
'not' (('not' ('not' (c . x1))) '&' ('not' (b . x1))) is boolean set
(a '&' b) . x1 is boolean Element of BOOLEAN
TRUE '&' TRUE is boolean Element of BOOLEAN
B_SUP ((a '&' b),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((a '&' b),(CompF (PA,G)))) . 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))
'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))
c 'imp' ('not' b) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'imp' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'imp' ('not' c) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
PA is a_partition of Y
All ((c 'imp' ('not' b)),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
All ((a 'imp' b),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(All ((c 'imp' ('not' b)),PA,G)) '&' (All ((a 'imp' b),PA,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
All ((a 'imp' ('not' c)),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
z is Element of Y
((All ((c 'imp' ('not' b)),PA,G)) '&' (All ((a 'imp' b),PA,G))) . z is boolean Element of BOOLEAN
(All ((a 'imp' ('not' c)),PA,G)) . z is boolean Element of BOOLEAN
(All ((c 'imp' ('not' b)),PA,G)) . z is boolean Element of BOOLEAN
(All ((a 'imp' b),PA,G)) . z is boolean Element of BOOLEAN
((All ((c 'imp' ('not' b)),PA,G)) . z) '&' ((All ((a 'imp' b),PA,G)) . z) is boolean Element of BOOLEAN
CompF (PA,G) is a_partition of Y
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
B_INF ((a 'imp' b),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((a 'imp' b),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
x1 is Element of Y
(a 'imp' b) . x1 is boolean Element of BOOLEAN
B_INF ((c 'imp' ('not' b)),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' ('not' b)),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
x1 is Element of Y
(c 'imp' ('not' b)) . x1 is boolean Element of BOOLEAN
x1 is Element of Y
(a 'imp' ('not' c)) . x1 is boolean Element of BOOLEAN
c . x1 is boolean Element of BOOLEAN
'not' (c . x1) is boolean Element of BOOLEAN
a . x1 is boolean Element of BOOLEAN
'not' (a . x1) is boolean Element of BOOLEAN
(c 'imp' ('not' b)) . x1 is boolean Element of BOOLEAN
('not' b) . x1 is boolean Element of BOOLEAN
('not' (c . x1)) 'or' (('not' b) . x1) is set
'not' ('not' (c . x1)) is boolean set
'not' (('not' b) . x1) is boolean set
('not' ('not' (c . x1))) '&' ('not' (('not' b) . x1)) is set
'not' (('not' ('not' (c . x1))) '&' ('not' (('not' b) . x1))) is boolean set
(a 'imp' b) . x1 is boolean Element of BOOLEAN
b . x1 is boolean Element of BOOLEAN
('not' (a . x1)) 'or' (b . x1) is set
'not' ('not' (a . x1)) is boolean set
'not' (b . x1) is boolean set
('not' ('not' (a . x1))) '&' ('not' (b . x1)) is set
'not' (('not' ('not' (a . x1))) '&' ('not' (b . x1))) is boolean set
('not' c) . x1 is boolean Element of BOOLEAN
TRUE 'or' TRUE is set
'not' TRUE is boolean set
('not' TRUE) '&' ('not' TRUE) is set
'not' (('not' TRUE) '&' ('not' TRUE)) is boolean set
('not' c) . x1 is boolean Element of BOOLEAN
('not' (a . x1)) 'or' TRUE is set
'not' TRUE is boolean set
('not' ('not' (a . x1))) '&' ('not' TRUE) is set
'not' (('not' ('not' (a . x1))) '&' ('not' TRUE)) is boolean set
('not' c) . x1 is boolean Element of BOOLEAN
TRUE 'or' (('not' c) . x1) is set
'not' TRUE is boolean set
'not' (('not' c) . x1) is boolean set
('not' TRUE) '&' ('not' (('not' c) . x1)) is set
'not' (('not' TRUE) '&' ('not' (('not' c) . x1))) is boolean set
'not' (b . x1) is boolean Element of BOOLEAN
B_INF ((a 'imp' ('not' c)),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((a 'imp' ('not' c)),(CompF (PA,G)))) . 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))
'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 'imp' 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 V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'imp' ('not' b) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'imp' ('not' c) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
PA is a_partition of Y
All ((c 'imp' b),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
All ((a 'imp' ('not' b)),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(All ((c 'imp' b),PA,G)) '&' (All ((a 'imp' ('not' b)),PA,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
All ((a 'imp' ('not' c)),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
z is Element of Y
((All ((c 'imp' b),PA,G)) '&' (All ((a 'imp' ('not' b)),PA,G))) . z is boolean Element of BOOLEAN
(All ((a 'imp' ('not' c)),PA,G)) . z is boolean Element of BOOLEAN
(All ((c 'imp' b),PA,G)) . z is boolean Element of BOOLEAN
(All ((a 'imp' ('not' b)),PA,G)) . z is boolean Element of BOOLEAN
((All ((c 'imp' b),PA,G)) . z) '&' ((All ((a 'imp' ('not' b)),PA,G)) . z) is boolean Element of BOOLEAN
CompF (PA,G) is a_partition of Y
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
B_INF ((a 'imp' ('not' b)),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((a 'imp' ('not' b)),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
x1 is Element of Y
(a 'imp' ('not' b)) . x1 is boolean Element of BOOLEAN
B_INF ((c 'imp' b),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' b),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
x1 is Element of Y
(c 'imp' b) . x1 is boolean Element of BOOLEAN
x1 is Element of Y
(a 'imp' ('not' c)) . x1 is boolean Element of BOOLEAN
c . x1 is boolean Element of BOOLEAN
'not' (c . x1) is boolean Element of BOOLEAN
a . x1 is boolean Element of BOOLEAN
'not' (a . x1) is boolean Element of BOOLEAN
(c 'imp' b) . x1 is boolean Element of BOOLEAN
b . x1 is boolean Element of BOOLEAN
('not' (c . x1)) 'or' (b . x1) is set
'not' ('not' (c . x1)) is boolean set
'not' (b . x1) is boolean set
('not' ('not' (c . x1))) '&' ('not' (b . x1)) is set
'not' (('not' ('not' (c . x1))) '&' ('not' (b . x1))) is boolean set
(a 'imp' ('not' b)) . x1 is boolean Element of BOOLEAN
('not' b) . x1 is boolean Element of BOOLEAN
('not' (a . x1)) 'or' (('not' b) . x1) is set
'not' ('not' (a . x1)) is boolean set
'not' (('not' b) . x1) is boolean set
('not' ('not' (a . x1))) '&' ('not' (('not' b) . x1)) is set
'not' (('not' ('not' (a . x1))) '&' ('not' (('not' b) . x1))) is boolean set
('not' c) . x1 is boolean Element of BOOLEAN
TRUE 'or' TRUE is set
'not' TRUE is boolean set
('not' TRUE) '&' ('not' TRUE) is set
'not' (('not' TRUE) '&' ('not' TRUE)) is boolean set
('not' c) . x1 is boolean Element of BOOLEAN
('not' (a . x1)) 'or' TRUE is set
'not' TRUE is boolean set
('not' ('not' (a . x1))) '&' ('not' TRUE) is set
'not' (('not' ('not' (a . x1))) '&' ('not' TRUE)) is boolean set
('not' c) . x1 is boolean Element of BOOLEAN
TRUE 'or' (('not' c) . x1) is set
'not' TRUE is boolean set
'not' (('not' c) . x1) is boolean set
('not' TRUE) '&' ('not' (('not' c) . x1)) is set
'not' (('not' TRUE) '&' ('not' (('not' c) . x1))) is boolean set
'not' (b . x1) is boolean Element of BOOLEAN
B_INF ((a 'imp' ('not' c)),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((a 'imp' ('not' c)),(CompF (PA,G)))) . 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))
'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))
c 'imp' ('not' b) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' ('not' c) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
PA is a_partition of Y
All ((c 'imp' ('not' b)),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Ex ((a '&' b),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(All ((c 'imp' ('not' b)),PA,G)) '&' (Ex ((a '&' b),PA,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Ex ((a '&' ('not' c)),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
z is Element of Y
((All ((c 'imp' ('not' b)),PA,G)) '&' (Ex ((a '&' b),PA,G))) . z is boolean Element of BOOLEAN
(Ex ((a '&' ('not' c)),PA,G)) . z is boolean Element of BOOLEAN
(All ((c 'imp' ('not' b)),PA,G)) . z is boolean Element of BOOLEAN
(Ex ((a '&' b),PA,G)) . z is boolean Element of BOOLEAN
((All ((c 'imp' ('not' b)),PA,G)) . z) '&' ((Ex ((a '&' b),PA,G)) . z) is boolean Element of BOOLEAN
CompF (PA,G) is a_partition of Y
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
B_SUP ((a '&' b),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((a '&' b),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
x1 is Element of Y
(a '&' b) . x1 is boolean Element of BOOLEAN
x1 is Element of Y
(a '&' b) . x1 is boolean Element of BOOLEAN
a . x1 is boolean Element of BOOLEAN
b . x1 is boolean Element of BOOLEAN
(a . x1) '&' (b . x1) is boolean Element of BOOLEAN
B_INF ((c 'imp' ('not' b)),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' ('not' b)),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
c₉ is Element of Y
(c 'imp' ('not' b)) . c₉ is boolean Element of BOOLEAN
(c 'imp' ('not' b)) . x1 is boolean Element of BOOLEAN
c . x1 is boolean Element of BOOLEAN
'not' (c . x1) is boolean Element of BOOLEAN
('not' b) . x1 is boolean Element of BOOLEAN
('not' (c . x1)) 'or' (('not' b) . x1) is set
'not' ('not' (c . x1)) is boolean set
'not' (('not' b) . x1) is boolean set
('not' ('not' (c . x1))) '&' ('not' (('not' b) . x1)) is set
'not' (('not' ('not' (c . x1))) '&' ('not' (('not' b) . x1))) is boolean set
(a '&' ('not' c)) . x1 is boolean Element of BOOLEAN
('not' c) . x1 is boolean Element of BOOLEAN
(a . x1) '&' (('not' c) . x1) is boolean Element of BOOLEAN
TRUE '&' TRUE is boolean Element of BOOLEAN
B_SUP ((a '&' ('not' c)),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((a '&' ('not' c)),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
'not' (b . x1) 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))
c 'imp' 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 V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' ('not' b) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' ('not' c) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
PA is a_partition of Y
All ((c 'imp' b),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Ex ((a '&' ('not' b)),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(All ((c 'imp' b),PA,G)) '&' (Ex ((a '&' ('not' b)),PA,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Ex ((a '&' ('not' c)),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
z is Element of Y
((All ((c 'imp' b),PA,G)) '&' (Ex ((a '&' ('not' b)),PA,G))) . z is boolean Element of BOOLEAN
(Ex ((a '&' ('not' c)),PA,G)) . z is boolean Element of BOOLEAN
(All ((c 'imp' b),PA,G)) . z is boolean Element of BOOLEAN
(Ex ((a '&' ('not' b)),PA,G)) . z is boolean Element of BOOLEAN
((All ((c 'imp' b),PA,G)) . z) '&' ((Ex ((a '&' ('not' b)),PA,G)) . z) is boolean Element of BOOLEAN
CompF (PA,G) is a_partition of Y
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
B_SUP ((a '&' ('not' b)),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((a '&' ('not' b)),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
x1 is Element of Y
(a '&' ('not' b)) . x1 is boolean Element of BOOLEAN
x1 is Element of Y
(a '&' ('not' b)) . x1 is boolean Element of BOOLEAN
a . x1 is boolean Element of BOOLEAN
('not' b) . x1 is boolean Element of BOOLEAN
(a . x1) '&' (('not' b) . x1) is boolean Element of BOOLEAN
B_INF ((c 'imp' b),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' b),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
c₉ is Element of Y
(c 'imp' b) . c₉ is boolean Element of BOOLEAN
(c 'imp' b) . x1 is boolean Element of BOOLEAN
c . x1 is boolean Element of BOOLEAN
'not' (c . x1) is boolean Element of BOOLEAN
b . x1 is boolean Element of BOOLEAN
('not' (c . x1)) 'or' (b . x1) is set
'not' ('not' (c . x1)) is boolean set
'not' (b . x1) is boolean set
('not' ('not' (c . x1))) '&' ('not' (b . x1)) is set
'not' (('not' ('not' (c . x1))) '&' ('not' (b . x1))) is boolean set
(a '&' ('not' c)) . x1 is boolean Element of BOOLEAN
('not' c) . x1 is boolean Element of BOOLEAN
(a . x1) '&' (('not' c) . x1) is boolean Element of BOOLEAN
TRUE '&' TRUE is boolean Element of BOOLEAN
B_SUP ((a '&' ('not' c)),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((a '&' ('not' c)),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
'not' (b . x1) 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 V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c 'imp' a is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
PA is a_partition of Y
Ex (c,PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
All ((c 'imp' b),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
All ((c 'imp' a),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
((Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G))) '&' (All ((c 'imp' a),PA,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Ex ((a '&' b),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
z is Element of Y
(((Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G))) '&' (All ((c 'imp' a),PA,G))) . z is boolean Element of BOOLEAN
(Ex ((a '&' b),PA,G)) . z is boolean Element of BOOLEAN
((Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G))) . z is boolean Element of BOOLEAN
(All ((c 'imp' a),PA,G)) . z is boolean Element of BOOLEAN
(((Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G))) . z) '&' ((All ((c 'imp' a),PA,G)) . z) is boolean Element of BOOLEAN
(Ex (c,PA,G)) . z is boolean Element of BOOLEAN
(All ((c 'imp' b),PA,G)) . z is boolean Element of BOOLEAN
((Ex (c,PA,G)) . z) '&' ((All ((c 'imp' b),PA,G)) . z) is boolean Element of BOOLEAN
(((Ex (c,PA,G)) . z) '&' ((All ((c 'imp' b),PA,G)) . z)) '&' ((All ((c 'imp' a),PA,G)) . z) is boolean Element of BOOLEAN
CompF (PA,G) is a_partition of Y
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
B_SUP (c,(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP (c,(CompF (PA,G)))) . z is boolean Element of BOOLEAN
x1 is Element of Y
c . x1 is boolean Element of BOOLEAN
x1 is Element of Y
c . x1 is boolean Element of BOOLEAN
'not' (c . x1) is boolean Element of BOOLEAN
B_INF ((c 'imp' b),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' b),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
c₉ is Element of Y
(c 'imp' b) . c₉ is boolean Element of BOOLEAN
(c 'imp' b) . x1 is boolean Element of BOOLEAN
b . x1 is boolean Element of BOOLEAN
('not' (c . x1)) 'or' (b . x1) is set
'not' ('not' (c . x1)) is boolean set
'not' (b . x1) is boolean set
('not' ('not' (c . x1))) '&' ('not' (b . x1)) is set
'not' (('not' ('not' (c . x1))) '&' ('not' (b . x1))) is boolean set
B_INF ((c 'imp' a),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' a),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
c₉ is Element of Y
(c 'imp' a) . c₉ is boolean Element of BOOLEAN
(c 'imp' a) . x1 is boolean Element of BOOLEAN
a . x1 is boolean Element of BOOLEAN
('not' (c . x1)) 'or' (a . x1) is set
'not' (a . x1) is boolean set
('not' ('not' (c . x1))) '&' ('not' (a . x1)) is set
'not' (('not' ('not' (c . x1))) '&' ('not' (a . x1))) is boolean set
(a '&' b) . x1 is boolean Element of BOOLEAN
TRUE '&' TRUE is boolean Element of BOOLEAN
B_SUP ((a '&' b),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((a '&' b),(CompF (PA,G)))) . 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))
'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 'imp' b is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b 'imp' ('not' a) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'imp' ('not' c) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
PA is a_partition of Y
All ((c 'imp' b),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
All ((b 'imp' ('not' a)),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(All ((c 'imp' b),PA,G)) '&' (All ((b 'imp' ('not' a)),PA,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
All ((a 'imp' ('not' c)),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
z is Element of Y
((All ((c 'imp' b),PA,G)) '&' (All ((b 'imp' ('not' a)),PA,G))) . z is boolean Element of BOOLEAN
(All ((a 'imp' ('not' c)),PA,G)) . z is boolean Element of BOOLEAN
(All ((c 'imp' b),PA,G)) . z is boolean Element of BOOLEAN
(All ((b 'imp' ('not' a)),PA,G)) . z is boolean Element of BOOLEAN
((All ((c 'imp' b),PA,G)) . z) '&' ((All ((b 'imp' ('not' a)),PA,G)) . z) is boolean Element of BOOLEAN
CompF (PA,G) is a_partition of Y
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
B_INF ((c 'imp' b),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' b),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
x1 is Element of Y
(c 'imp' b) . x1 is boolean Element of BOOLEAN
B_INF ((b 'imp' ('not' a)),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((b 'imp' ('not' a)),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
x1 is Element of Y
(b 'imp' ('not' a)) . x1 is boolean Element of BOOLEAN
x1 is Element of Y
(a 'imp' ('not' c)) . x1 is boolean Element of BOOLEAN
b . x1 is boolean Element of BOOLEAN
'not' (b . x1) is boolean Element of BOOLEAN
c . x1 is boolean Element of BOOLEAN
'not' (c . x1) is boolean Element of BOOLEAN
(b 'imp' ('not' a)) . x1 is boolean Element of BOOLEAN
('not' a) . x1 is boolean Element of BOOLEAN
('not' (b . x1)) 'or' (('not' a) . x1) is set
'not' ('not' (b . x1)) is boolean set
'not' (('not' a) . x1) is boolean set
('not' ('not' (b . x1))) '&' ('not' (('not' a) . x1)) is set
'not' (('not' ('not' (b . x1))) '&' ('not' (('not' a) . x1))) is boolean set
(c 'imp' b) . x1 is boolean Element of BOOLEAN
('not' (c . x1)) 'or' (b . x1) is set
'not' ('not' (c . x1)) is boolean set
'not' (b . x1) is boolean set
('not' ('not' (c . x1))) '&' ('not' (b . x1)) is set
'not' (('not' ('not' (c . x1))) '&' ('not' (b . x1))) is boolean set
('not' c) . x1 is boolean Element of BOOLEAN
a . x1 is boolean Element of BOOLEAN
'not' (a . x1) is boolean Element of BOOLEAN
('not' (a . x1)) 'or' TRUE is set
'not' ('not' (a . x1)) is boolean set
'not' TRUE is boolean set
('not' ('not' (a . x1))) '&' ('not' TRUE) is set
'not' (('not' ('not' (a . x1))) '&' ('not' TRUE)) is boolean set
('not' c) . x1 is boolean Element of BOOLEAN
a . x1 is boolean Element of BOOLEAN
'not' (a . x1) is boolean Element of BOOLEAN
('not' (a . x1)) 'or' TRUE is set
'not' ('not' (a . x1)) is boolean set
'not' TRUE is boolean set
('not' ('not' (a . x1))) '&' ('not' TRUE) is set
'not' (('not' ('not' (a . x1))) '&' ('not' TRUE)) is boolean set
a . x1 is boolean Element of BOOLEAN
'not' (a . x1) is boolean Element of BOOLEAN
('not' c) . x1 is boolean Element of BOOLEAN
TRUE 'or' (('not' c) . x1) is set
'not' TRUE is boolean set
'not' (('not' c) . x1) is boolean set
('not' TRUE) '&' ('not' (('not' c) . x1)) is set
'not' (('not' TRUE) '&' ('not' (('not' c) . x1))) is boolean set
B_INF ((a 'imp' ('not' c)),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((a 'imp' ('not' c)),(CompF (PA,G)))) . 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 V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b 'imp' a is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' c is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
PA is a_partition of Y
Ex (c,PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
All ((c 'imp' b),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
All ((b 'imp' a),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
((Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G))) '&' (All ((b 'imp' a),PA,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Ex ((a '&' c),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
z is Element of Y
(((Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G))) '&' (All ((b 'imp' a),PA,G))) . z is boolean Element of BOOLEAN
(Ex ((a '&' c),PA,G)) . z is boolean Element of BOOLEAN
((Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G))) . z is boolean Element of BOOLEAN
(All ((b 'imp' a),PA,G)) . z is boolean Element of BOOLEAN
(((Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G))) . z) '&' ((All ((b 'imp' a),PA,G)) . z) is boolean Element of BOOLEAN
(Ex (c,PA,G)) . z is boolean Element of BOOLEAN
(All ((c 'imp' b),PA,G)) . z is boolean Element of BOOLEAN
((Ex (c,PA,G)) . z) '&' ((All ((c 'imp' b),PA,G)) . z) is boolean Element of BOOLEAN
(((Ex (c,PA,G)) . z) '&' ((All ((c 'imp' b),PA,G)) . z)) '&' ((All ((b 'imp' a),PA,G)) . z) is boolean Element of BOOLEAN
CompF (PA,G) is a_partition of Y
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
B_SUP (c,(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP (c,(CompF (PA,G)))) . z is boolean Element of BOOLEAN
x1 is Element of Y
c . x1 is boolean Element of BOOLEAN
x1 is Element of Y
c . x1 is boolean Element of BOOLEAN
b . x1 is boolean Element of BOOLEAN
'not' (b . x1) is boolean Element of BOOLEAN
B_INF ((b 'imp' a),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((b 'imp' a),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
c₉ is Element of Y
(b 'imp' a) . c₉ is boolean Element of BOOLEAN
(b 'imp' a) . x1 is boolean Element of BOOLEAN
a . x1 is boolean Element of BOOLEAN
('not' (b . x1)) 'or' (a . x1) is set
'not' ('not' (b . x1)) is boolean set
'not' (a . x1) is boolean set
('not' ('not' (b . x1))) '&' ('not' (a . x1)) is set
'not' (('not' ('not' (b . x1))) '&' ('not' (a . x1))) is boolean set
'not' (c . x1) is boolean Element of BOOLEAN
B_INF ((c 'imp' b),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' b),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
c₉ is Element of Y
(c 'imp' b) . c₉ is boolean Element of BOOLEAN
(c 'imp' b) . x1 is boolean Element of BOOLEAN
('not' (c . x1)) 'or' (b . x1) is set
'not' ('not' (c . x1)) is boolean set
'not' (b . x1) is boolean set
('not' ('not' (c . x1))) '&' ('not' (b . x1)) is set
'not' (('not' ('not' (c . x1))) '&' ('not' (b . x1))) is boolean set
(a '&' c) . x1 is boolean Element of BOOLEAN
TRUE '&' TRUE is boolean Element of BOOLEAN
B_SUP ((a '&' c),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((a '&' c),(CompF (PA,G)))) . 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))
'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))
b 'imp' ('not' c) 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 V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c 'imp' a is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' ('not' b) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
PA is a_partition of Y
Ex (c,PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
All ((b 'imp' ('not' c)),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Ex (c,PA,G)) '&' (All ((b 'imp' ('not' c)),PA,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
All ((c 'imp' a),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
((Ex (c,PA,G)) '&' (All ((b 'imp' ('not' c)),PA,G))) '&' (All ((c 'imp' a),PA,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Ex ((a '&' ('not' b)),PA,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
z is Element of Y
(((Ex (c,PA,G)) '&' (All ((b 'imp' ('not' c)),PA,G))) '&' (All ((c 'imp' a),PA,G))) . z is boolean Element of BOOLEAN
(Ex ((a '&' ('not' b)),PA,G)) . z is boolean Element of BOOLEAN
((Ex (c,PA,G)) '&' (All ((b 'imp' ('not' c)),PA,G))) . z is boolean Element of BOOLEAN
(All ((c 'imp' a),PA,G)) . z is boolean Element of BOOLEAN
(((Ex (c,PA,G)) '&' (All ((b 'imp' ('not' c)),PA,G))) . z) '&' ((All ((c 'imp' a),PA,G)) . z) is boolean Element of BOOLEAN
(Ex (c,PA,G)) . z is boolean Element of BOOLEAN
(All ((b 'imp' ('not' c)),PA,G)) . z is boolean Element of BOOLEAN
((Ex (c,PA,G)) . z) '&' ((All ((b 'imp' ('not' c)),PA,G)) . z) is boolean Element of BOOLEAN
(((Ex (c,PA,G)) . z) '&' ((All ((b 'imp' ('not' c)),PA,G)) . z)) '&' ((All ((c 'imp' a),PA,G)) . z) is boolean Element of BOOLEAN
CompF (PA,G) is a_partition of Y
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
B_SUP (c,(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP (c,(CompF (PA,G)))) . z is boolean Element of BOOLEAN
x1 is Element of Y
c . x1 is boolean Element of BOOLEAN
x1 is Element of Y
c . x1 is boolean Element of BOOLEAN
'not' (c . x1) is boolean Element of BOOLEAN
B_INF ((c 'imp' a),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((c 'imp' a),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
c₉ is Element of Y
(c 'imp' a) . c₉ is boolean Element of BOOLEAN
(c 'imp' a) . x1 is boolean Element of BOOLEAN
a . x1 is boolean Element of BOOLEAN
('not' (c . x1)) 'or' (a . x1) is set
'not' ('not' (c . x1)) is boolean set
'not' (a . x1) is boolean set
('not' ('not' (c . x1))) '&' ('not' (a . x1)) is set
'not' (('not' ('not' (c . x1))) '&' ('not' (a . x1))) is boolean set
b . x1 is boolean Element of BOOLEAN
'not' (b . x1) is boolean Element of BOOLEAN
B_INF ((b 'imp' ('not' c)),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_INF ((b 'imp' ('not' c)),(CompF (PA,G)))) . z is boolean Element of BOOLEAN
c₉ is Element of Y
(b 'imp' ('not' c)) . c₉ is boolean Element of BOOLEAN
(b 'imp' ('not' c)) . x1 is boolean Element of BOOLEAN
('not' c) . x1 is boolean Element of BOOLEAN
('not' (b . x1)) 'or' (('not' c) . x1) is set
'not' ('not' (b . x1)) is boolean set
'not' (('not' c) . x1) is boolean set
('not' ('not' (b . x1))) '&' ('not' (('not' c) . x1)) is set
'not' (('not' ('not' (b . x1))) '&' ('not' (('not' c) . x1))) is boolean set
(a '&' ('not' b)) . x1 is boolean Element of BOOLEAN
('not' b) . x1 is boolean Element of BOOLEAN
(a . x1) '&' (('not' b) . x1) is boolean Element of BOOLEAN
TRUE '&' TRUE is boolean Element of BOOLEAN
B_SUP ((a '&' ('not' b)),(CompF (PA,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((a '&' ('not' b)),(CompF (PA,G)))) . z is boolean Element of BOOLEAN