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

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

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(()) is set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
G is Element of K10(())
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

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

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

() '&' ('not' ((Ex (b,a,G)) . PA)) is set
'not' (() '&' ('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' ('not' ((All (c,a,G)) . PA))) '&' () is set
'not' (('not' ('not' ((All (c,a,G)) . PA))) '&' ()) 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(()) is set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
G is Element of K10(())
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

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(()) is set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
G is Element of K10(())
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

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(()) is set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
G is Element of K10(())
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)) '&' (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 ((),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Ex ((),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Ex ((),a,G)) 'or' (Ex ((),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 ((),a,G)) 'or' (Ex ((),a,G))) . PA is boolean Element of BOOLEAN
('not' ((All (c,a,G)) '&' (All (b,a,G)))) . PA is boolean Element of BOOLEAN
(Ex ((),a,G)) . PA is boolean Element of BOOLEAN
(Ex ((),a,G)) . PA is boolean Element of BOOLEAN
((Ex ((),a,G)) . PA) 'or' ((Ex ((),a,G)) . PA) is set
'not' ((Ex ((),a,G)) . PA) is boolean set
'not' ((Ex ((),a,G)) . PA) is boolean set
('not' ((Ex ((),a,G)) . PA)) '&' ('not' ((Ex ((),a,G)) . PA)) is set
'not' (('not' ((Ex ((),a,G)) . PA)) '&' ('not' ((Ex ((),a,G)) . PA))) is boolean set
EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)
B_SUP ((),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
z is Element of Y
() . z is boolean Element of BOOLEAN
z is Element of Y
() . 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

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)
B_SUP ((),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
z is Element of Y
() . z is boolean Element of BOOLEAN
z is Element of Y
() . 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

PA is Element of Y
('not' ((All (c,a,G)) '&' (All (b,a,G)))) . PA is boolean Element of BOOLEAN
((Ex ((),a,G)) 'or' (Ex ((),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
() . z is boolean Element of BOOLEAN
B_SUP ((),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
(Ex ((),a,G)) . PA is boolean Element of BOOLEAN
(Ex ((),a,G)) . PA is boolean Element of BOOLEAN
TRUE 'or' ((Ex ((),a,G)) . PA) is set

'not' ((Ex ((),a,G)) . PA) is boolean set
() '&' ('not' ((Ex ((),a,G)) . PA)) is set
'not' (() '&' ('not' ((Ex ((),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
() . z is boolean Element of BOOLEAN
B_SUP ((),(CompF (a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(B_SUP ((),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
(Ex ((),a,G)) . PA is boolean Element of BOOLEAN
(Ex ((),a,G)) . PA is boolean Element of BOOLEAN
((Ex ((),a,G)) . PA) 'or' TRUE is set
'not' ((Ex ((),a,G)) . PA) is boolean set

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

EqClass (PA,(CompF (a,G))) is Element of CompF (a,G)
(B_INF ((),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
z is Element of Y
() . z is boolean Element of BOOLEAN
z is Element of Y
() . 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

B_INF ((),(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 ((),a,G)) 'or' (All ((),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
() . z is boolean Element of BOOLEAN
(All ((),a,G)) . PA is boolean Element of BOOLEAN
(All ((),a,G)) . PA is boolean Element of BOOLEAN
((All ((),a,G)) . PA) 'or' ((All ((),a,G)) . PA) is set
'not' ((All ((),a,G)) . PA) is boolean set
'not' ((All ((),a,G)) . PA) is boolean set
('not' ((All ((),a,G)) . PA)) '&' ('not' ((All ((),a,G)) . PA)) is set
'not' (('not' ((All ((),a,G)) . PA)) '&' ('not' ((All ((),a,G)) . PA))) is boolean set
TRUE 'or' ((All ((),a,G)) . PA) is set

() '&' ('not' ((All ((),a,G)) . PA)) is set
'not' (() '&' ('not' ((All ((),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
() . z is boolean Element of BOOLEAN
(All ((),a,G)) . PA is boolean Element of BOOLEAN
(All ((),a,G)) . PA is boolean Element of BOOLEAN
((All ((),a,G)) . PA) 'or' ((All ((),a,G)) . PA) is set
'not' ((All ((),a,G)) . PA) is boolean set
'not' ((All ((),a,G)) . PA) is boolean set
('not' ((All ((),a,G)) . PA)) '&' ('not' ((All ((),a,G)) . PA)) is set
'not' (('not' ((All ((),a,G)) . PA)) '&' ('not' ((All ((),a,G)) . PA))) is boolean set
((All ((),a,G)) . PA) 'or' TRUE is set

('not' ((All ((),a,G)) . PA)) '&' () is set
'not' (('not' ((All ((),a,G)) . PA)) '&' ()) 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(()) is set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
G is Element of K10(())
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' (b . PA)) is set
'not' (() '&' ('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' (c . PA)) '&' () is set
'not' (('not' (c . PA)) '&' ()) 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(()) is set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
G is Element of K10(())
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' ((Ex (b,a,G)) . PA)) is set
'not' (() '&' ('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' ((Ex (c,a,G)) . PA)) '&' () is set
'not' (('not' ((Ex (c,a,G)) . PA)) '&' ()) 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(()) is set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
G is Element of K10(())
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))

a is a_partition of Y
Ex ((),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 ((),a,G)) 'xor' (Ex (b,a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ((Ex ((),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 ((),a,G) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Ex (c,a,G)) 'xor' (Ex ((),a,G)) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ((Ex (c,a,G)) 'xor' (Ex ((),a,G))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' ((Ex ((),a,G)) 'xor' (Ex (b,a,G)))) 'or' ('not' ((Ex (c,a,G)) 'xor' (Ex ((),a,G)))) is V12() quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
CompF (a,G) is a_partition of Y
B_SUP ((),(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 ((),a,G)) 'xor' (Ex (b,a,G)))) 'or' ('not' ((Ex (c,a,G)) 'xor' (Ex ((),a,G))))) . PA is boolean Element of BOOLEAN
B_SUP ((),(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)

() . PA is boolean Element of BOOLEAN
(B_SUP ((),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
('not' ((Ex (c,a,G)) 'xor' (Ex ((),a,G)))) . PA is boolean Element of BOOLEAN
((Ex (c,a,G)) 'xor' (Ex ((),a,G))) . PA is boolean Element of BOOLEAN
'not' (((Ex (c,a,G)) 'xor' (Ex ((),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 ((),a,G)) 'xor' (Ex (b,a,G))) . PA is boolean Element of BOOLEAN
(Ex ((),a,G)) . PA is boolean Element of BOOLEAN
((Ex ((),a,G)) . PA) 'xor' ((Ex (b,a,G)) . PA) is set
((Ex ((),a,G)) . PA) <=> ((Ex (b,a,G)) . PA) is set
'not' (((Ex ((),a,G)) . PA) 'xor' ((Ex (b,a,G)) . PA)) is boolean set
((Ex ((),a,G)) . PA) => ((Ex (b,a,G)) . PA) is set
'not' ((Ex ((),a,G)) . PA) is boolean set
('not' ((Ex ((),a,G)) . PA)) 'or' ((Ex (b,a,G)) . PA) is set
'not' ('not' ((Ex ((),a,G)) . PA)) is boolean set
'not' ((Ex (b,a,G)) . PA) is boolean set
('not' ('not' ((Ex ((),a,G)) . PA))) '&' ('not' ((Ex (b,a,G)) . PA)) is set
'not' (('not' ('not' ((Ex ((),a,G)) . PA))) '&' ('not' ((Ex (b,a,G)) . PA))) is boolean set
((Ex (b,a,G)) . PA) => ((Ex ((),a,G)) . PA) is set
('not' ((Ex (b,a,G)) . PA)) 'or' ((Ex ((),a,G)) . PA) is set
'not' ('not' ((Ex (b,a,G)) . PA)) is boolean set
('not' ('not' ((Ex (b,a,G)) . PA))) '&' ('not' ((Ex ((),a,G)) . PA)) is set
'not' (('not' ('not' ((Ex (b,a,G)) . PA))) '&' ('not' ((Ex ((),a,G)) . PA))) is boolean set
(((Ex ((),a,G)) . PA) => ((Ex (b,a,G)) . PA)) '&' (((Ex (b,a,G)) . PA) => ((Ex ((),a,G)) . PA)) is set
'not' (((Ex ((),a,G)) . PA) <=> ((Ex (b,a,G)) . PA)) is boolean set
('not' ((Ex ((),a,G)) 'xor' (Ex (b,a,G)))) . PA is boolean Element of BOOLEAN
(('not' ((Ex ((),a,G)) 'xor' (Ex (b,a,G)))) . PA) 'or' (('not' ((Ex (c,a,G)) 'xor' (Ex ((),a,G)))) . PA) is set
'not' (('not' ((Ex ((),a,G)) 'xor' (Ex (b,a,G)))) . PA) is boolean set
'not' (('not' ((Ex (c,a,G)) 'xor' (Ex ((),a,G)))) . PA) is boolean set
('not' (('not' ((Ex ((),a,G)) 'xor' (Ex (b,a,G)))) . PA)) '&' ('not' (('not' ((Ex (c,a,G)) 'xor' (Ex ((),a,G)))) . PA)) is set
'not' (('not' (('not' ((Ex ((),a,G)) 'xor' (Ex (b,a,G)))) . PA)) '&' ('not' (('not' ((Ex (c,a,G)) 'xor' (Ex ((),a,G)))) . PA))) is boolean set

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

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

() '&' ('not' ('not' (((Ex (c,a,G)) 'xor' (Ex ((),a,G))) . PA))) is set
'not' (() '&' ('not' ('not' (((Ex (c,a,G)) 'xor' (Ex ((),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 ((),a,G)))) . PA is boolean Element of BOOLEAN
((Ex (c,a,G)) 'xor' (Ex ((),a,G))) . PA is boolean Element of BOOLEAN
'not' (((Ex (c,a,G)) 'xor' (Ex ((),a,G))) . PA) is boolean Element of BOOLEAN
() . PA is boolean Element of BOOLEAN
(B_SUP ((),(CompF (a,G)))) . PA is boolean Element of BOOLEAN
(Ex ((),a,G)) . PA is boolean Element of BOOLEAN
((Ex (c,a,G)) . PA) 'xor' ((Ex ((),a,G)) . PA) is set
((Ex (c,a,G)) . PA) <=> ((Ex ((),a,G)) . PA) is set
'not' (((Ex (c,a,G)) . PA) 'xor' ((Ex ((),a,G)) . PA)) is boolean set
((Ex (c,a,G)) . PA) => ((Ex ((),a,G)) . PA) is set
'not' ((Ex (c,a,G)) . PA) is boolean set
('not' ((Ex (c,a,G)) . PA)) 'or' ((Ex ((),a,G)) . PA) is set
'not' ('not' ((Ex (c,a,G)) . PA)) is boolean set
'not' ((Ex ((),a,G)) . PA) is boolean set
('not' ('not' ((Ex (c,a,G)) . PA))) '&' ('not' ((Ex ((),a,G)) . PA)) is set
'not' (('not' ('not' ((Ex (c,a,G)) . PA))) '&' ('not' ((Ex ((),a,G)) . PA))) is boolean set
((Ex ((),a,G)) . PA) => ((Ex (c,a,G)) . PA) is set
('not' ((Ex ((),a,G)) . PA)) 'or' ((Ex (c,a,G)) . PA) is set
'not' ('not' ((Ex ((),a,G)) . PA)) is boolean set
('not' ('not' ((Ex ((),a,G)) . PA))) '&' ('not' ((Ex (c,a,G)) . PA)) is set
'not' (('not' ('not' ((Ex ((),a,G)) . PA))) '&' ('not' ((Ex (c,a,G)) . PA))) is boolean set
(((Ex (c,a,G)) . PA) => ((Ex ((),a,G)) . PA)) '&' (((Ex ((),a,G)) . PA) => ((Ex (c,a,G)) . PA)) is set
'not' (((Ex (c,a,G)) . PA) <=> ((Ex ((),a,G)) . PA)) is boolean set
('not' ((Ex ((),a,G)) 'xor' (Ex (b,a,G)))) . PA is boolean Element of BOOLEAN
(('not' ((Ex ((),a,G)) 'xor' (Ex (b,a,G)))) . PA) 'or' (('not' ((Ex (c,a,G)) 'xor' (Ex ((),a,G)))) . PA) is set
'not' (('not' ((Ex ((),a,G)) 'xor' (Ex (b,a,G)))) . PA) is boolean set
'not' (('not' ((Ex (c,a,G)) 'xor' (Ex ((),a,G)))) . PA) is boolean set
('not' (('not' ((Ex ((),a,G)) 'xor' (Ex (b,a,G)))) . PA)) '&' ('not' (('not' ((Ex (c,a,G)) 'xor' (Ex ((),a,G)))) . PA)) is set
'not' (('not' (('not' ((Ex ((),a,G)) 'xor' (Ex (b,a,G)))) . PA)) '&' ('not' (('not' ((Ex (c,a,G)) 'xor' (Ex ((),a,G)))) . PA))) is boolean set
((Ex ((),a,G)) 'xor' (Ex (b,a,G))) . PA is boolean Element of BOOLEAN
'not' (((Ex ((),a,G)) 'xor' (Ex (b,a,G))) . PA) is boolean Element of BOOLEAN

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

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

('not' ('not' (((Ex ((),a,G)) 'xor' (Ex (b,a,G))) . PA))) '&' () is set
'not' (('not' ('not' (((Ex ((),a,G)) 'xor' (Ex (b,a,G))) . PA))) '&' ()) 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(()) is set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
G is Element of K10(())
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' ((All (c,a,G)) . PA)) '&' () is set
'not' (('not' ((All (c,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
(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' ((Ex (b,a,G)) . PA) is boolean set
() '&' ('not' ((Ex (b,a,G)) . PA)) is set
'not' (() '&' ('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

() '&' () is set
'not' (() '&' ()) 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
c9 is Element of Y
b . c9 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(()) 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(())
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(()) is set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
G is Element of K10(())
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' ((All (b,a,G)) . PA) is boolean set
() '&' ('not' ((All (b,a,G)) . PA)) is set
'not' (() '&' ('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' ((Ex (c,a,G)) . PA)) '&' () is set
'not' (('not' ((Ex (c,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
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

() '&' () is set
'not' (() '&' ()) 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
c9 is Element of Y
c . c9 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(()) is set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
G is Element of K10(())
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' ((Ex (b,a,G)) . PA) is boolean set
() '&' ('not' ((Ex (b,a,G)) . PA)) is set
'not' (() '&' ('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' ((Ex (c,a,G)) . PA)) '&' () is set
'not' (('not' ((Ex (c,a,G)) . PA)) '&' ()) 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(()) is set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
G is Element of K10(())
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

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(()) is set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
G is Element of K10(())
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

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(()) 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(())
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(()) is set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
G is Element of K10(())
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' ('not' ((All (c,a,G)) . PA))) '&' () is set
'not' (('not' ('not' ((All (c,a,G)) . PA))) '&' ()) 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

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

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

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

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

() '&' ('not' ((Ex (b,a,G)) . PA)) is set
'not' (() '&' ('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
c9 is Element of Y
b . c9 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(()) is set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
G is Element of K10(())
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' ('not' ((Ex (c,a,G)) . PA))) '&' () is set
'not' (('not' ('not' ((Ex (c,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
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)