:: BVFUNC11 semantic presentation

K128() is Element of bool K124()
K124() is set
bool K124() is set
K123() is set
bool K123() is set
bool K128() is set
BOOLEAN is non empty set
{} is empty V56() set
the empty V56() set is empty V56() set
{{}} is non empty set
TRUE is boolean Element of BOOLEAN
1 is non empty set
FALSE is boolean Element of BOOLEAN
K129() is empty V56() Element of K128()
K174() is set
K175() is set
Y is non empty set
a is Element of Y
G is non empty with_non-empty_elements a_partition of Y
A is non empty with_non-empty_elements a_partition of Y
EqClass (a,G) is Element of G
EqClass (a,A) is Element of A
B is set
Y is non empty set
a is Element of Y
G is non empty with_non-empty_elements a_partition of Y
EqClass (a,G) is Element of G
A is non empty with_non-empty_elements a_partition of Y
G '\/' A is non empty with_non-empty_elements a_partition of Y
EqClass (a,(G '\/' A)) is Element of G '\/' A
Y is non empty set
a is Element of Y
G is non empty with_non-empty_elements a_partition of Y
A is non empty with_non-empty_elements a_partition of Y
G '/\' A is non empty with_non-empty_elements a_partition of Y
EqClass (a,(G '/\' A)) is Element of G '/\' A
EqClass (a,G) is Element of G
Y is non empty set
A is non empty set
a is Element of Y
G is non empty with_non-empty_elements a_partition of Y
EqClass (a,G) is Element of G
%O Y is non empty with_non-empty_elements a_partition of Y
EqClass (a,(%O Y)) is Element of %O Y
B is Element of A
SmallestPartition A is non empty with_non-empty_elements a_partition of A
EqClass (B,(SmallestPartition A)) is Element of SmallestPartition A
z is non empty with_non-empty_elements a_partition of A
EqClass (B,z) is Element of z
Y is non empty set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Element of bool (PARTITIONS Y)
G is non empty with_non-empty_elements a_partition of Y
A is non empty with_non-empty_elements a_partition of Y
{G,A} is non empty set
B is set
z is set
(G,A) --> (B,z) is Relation-like Function-like set
SS is set
((G,A) --> (B,z)) . SS is set
{B,z} is non empty set
SS is set
dom ((G,A) --> (B,z)) is set
rng ((G,A) --> (B,z)) is set
SS is Element of bool (bool Y)
Intersect SS is Element of bool Y
B /\ z is set
Y is non empty set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Element of bool (PARTITIONS Y)
'/\' a is non empty with_non-empty_elements a_partition of Y
G is non empty with_non-empty_elements a_partition of Y
A is non empty with_non-empty_elements a_partition of Y
{G,A} is non empty set
G '/\' A is non empty with_non-empty_elements a_partition of Y
B is set
z is Relation-like Function-like set
dom z is set
rng z is set
x is Element of bool (bool Y)
Intersect x is Element of bool Y
z . G is set
meet (rng z) is set
z . A is set
(z . G) /\ (z . A) is set
{(z . G),(z . A)} is non empty set
SS is set
h is set
z . h is set
SS is set
SS is set
h is set
SS is set
INTERSECTION (G,A) is set
(INTERSECTION (G,A)) \ {{}} is Element of bool (INTERSECTION (G,A))
bool (INTERSECTION (G,A)) is set
B is set
INTERSECTION (G,A) is set
(INTERSECTION (G,A)) \ {{}} is Element of bool (INTERSECTION (G,A))
bool (INTERSECTION (G,A)) is set
z is set
x is set
z /\ x is set
{z,x} is non empty set
SS is set
SS is Element of bool (bool Y)
Intersect SS is Element of bool Y
(G,A) --> (z,x) is Relation-like Function-like set
d is set
((G,A) --> (z,x)) . d is set
dom ((G,A) --> (z,x)) is set
rng ((G,A) --> (z,x)) is set
Y is non empty set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Element of bool (PARTITIONS Y)
G is non empty with_non-empty_elements a_partition of Y
A is non empty with_non-empty_elements a_partition of Y
{G,A} is non empty set
CompF (G,a) is non empty with_non-empty_elements a_partition of Y
{A} is non empty Element of bool (PARTITIONS Y)
'/\' {A} is non empty with_non-empty_elements a_partition of Y
B is set
z is Relation-like Function-like set
dom z is set
rng z is set
x is Element of bool (bool Y)
Intersect x is Element of bool Y
z . A is set
{(z . A)} is non empty set
meet {(z . A)} is set
B is set
A .--> B is trivial Relation-like {A} -defined Function-like one-to-one set
{A} is non empty set
{A} --> B is non empty Relation-like {A} -defined Function-like constant V17({A}) quasi_total Element of bool [:{A},{B}:]
{B} is non empty set
[:{A},{B}:] is set
bool [:{A},{B}:] is set
dom (A .--> B) is set
x is set
(A .--> B) . x is set
rng (A .--> B) is set
x is set
x is Element of bool (bool Y)
meet x is Element of bool Y
Intersect x is Element of bool Y
{G} is non empty Element of bool (PARTITIONS Y)
{G} \ {G} is Element of bool (PARTITIONS Y)
a \ {G} is Element of bool (PARTITIONS Y)
{G} \/ {A} is non empty Element of bool (PARTITIONS Y)
({G} \/ {A}) \ {G} is Element of bool (PARTITIONS Y)
{A} \ {G} is Element of bool (PARTITIONS Y)
({G} \ {G}) \/ ({A} \ {G}) is Element of bool (PARTITIONS Y)
({G} \ {G}) \/ {A} is non empty Element of bool (PARTITIONS Y)
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
A is Element of bool (PARTITIONS Y)
B is non empty with_non-empty_elements a_partition of Y
All (a,B,A) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (G,B,A) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (G,B,A) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
CompF (B,G) is non empty with_non-empty_elements a_partition of Y
B_SUP (a,(CompF (B,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
(All ((Ex (a,A,G)),B,G)) . z is boolean Element of BOOLEAN
(Ex ((Ex (a,B,G)),A,G)) . z is boolean Element of BOOLEAN
EqClass (z,(CompF (B,G))) is Element of CompF (B,G)
B_INF ((Ex (a,A,G)),(CompF (B,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(B_INF ((Ex (a,A,G)),(CompF (B,G)))) . z is boolean Element of BOOLEAN
x is Element of Y
(Ex (a,A,G)) . x is boolean Element of BOOLEAN
CompF (A,G) is non empty with_non-empty_elements a_partition of Y
EqClass (z,(CompF (A,G))) is Element of CompF (A,G)
B_SUP (a,(CompF (A,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(B_SUP (a,(CompF (A,G)))) . z is boolean Element of BOOLEAN
(Ex (a,A,G)) . z is boolean Element of BOOLEAN
x is Element of Y
a . x is boolean Element of BOOLEAN
x is Element of Y
a . x is boolean Element of BOOLEAN
EqClass (x,(CompF (B,G))) is Element of CompF (B,G)
(Ex (a,B,G)) . x is boolean Element of BOOLEAN
B_SUP ((Ex (a,B,G)),(CompF (A,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(B_SUP ((Ex (a,B,G)),(CompF (A,G)))) . z is boolean Element of BOOLEAN
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
CompF (A,G) is non empty with_non-empty_elements a_partition of Y
B_INF (a,(CompF (A,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
('not' (Ex ((All (a,A,G)),B,G))) . z is boolean Element of BOOLEAN
(Ex ((Ex (('not' a),B,G)),A,G)) . z is boolean Element of BOOLEAN
CompF (B,G) is non empty with_non-empty_elements a_partition of Y
EqClass (z,(CompF (B,G))) is Element of CompF (B,G)
(Ex ((All (a,A,G)),B,G)) . z is boolean Element of BOOLEAN
'not' ((Ex ((All (a,A,G)),B,G)) . z) is boolean Element of BOOLEAN
K105(1,((Ex ((All (a,A,G)),B,G)) . z)) is set
B_SUP ((All (a,A,G)),(CompF (B,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(All (a,A,G)) . z is boolean Element of BOOLEAN
EqClass (z,(CompF (A,G))) is Element of CompF (A,G)
x is Element of Y
a . x is boolean Element of BOOLEAN
('not' a) . x is boolean Element of BOOLEAN
'not' FALSE is boolean Element of BOOLEAN
K105(1,FALSE) is set
B_SUP (('not' a),(CompF (B,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
EqClass (x,(CompF (B,G))) is Element of CompF (B,G)
(Ex (('not' a),B,G)) . x is boolean Element of BOOLEAN
B_SUP ((Ex (('not' a),B,G)),(CompF (A,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(B_SUP ((Ex (('not' a),B,G)),(CompF (A,G)))) . z is boolean Element of BOOLEAN
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex (('not' (All (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All (('not' (All (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (All (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (All (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All (('not' (All (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
(All ((All (('not' a),A,G)),B,G)) . z is boolean Element of BOOLEAN
('not' (All ((All (a,B,G)),A,G))) . z is boolean Element of BOOLEAN
CompF (A,G) is non empty with_non-empty_elements a_partition of Y
EqClass (z,(CompF (A,G))) is Element of CompF (A,G)
CompF (B,G) is non empty with_non-empty_elements a_partition of Y
EqClass (z,(CompF (B,G))) is Element of CompF (B,G)
B_INF ((All (('not' a),A,G)),(CompF (B,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(B_INF ((All (('not' a),A,G)),(CompF (B,G)))) . z is boolean Element of BOOLEAN
x is Element of Y
(All (('not' a),A,G)) . x is boolean Element of BOOLEAN
B_INF (('not' a),(CompF (A,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(All (('not' a),A,G)) . z is boolean Element of BOOLEAN
('not' a) . z is boolean Element of BOOLEAN
a . z is boolean Element of BOOLEAN
'not' (a . z) is boolean Element of BOOLEAN
K105(1,(a . z)) is set
B_INF (a,(CompF (B,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(B_INF (a,(CompF (B,G)))) . z is boolean Element of BOOLEAN
(All (a,B,G)) . z is boolean Element of BOOLEAN
B_INF ((All (a,B,G)),(CompF (A,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(B_INF ((All (a,B,G)),(CompF (A,G)))) . z is boolean Element of BOOLEAN
(All ((All (a,B,G)),A,G)) . z is boolean Element of BOOLEAN
'not' ((All ((All (a,B,G)),A,G)) . z) is boolean Element of BOOLEAN
K105(1,((All ((All (a,B,G)),A,G)) . z)) is set
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((Ex (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
G is Element of bool (PARTITIONS Y)
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
('not' (Ex ((Ex (a,A,G)),B,G))) . z is boolean Element of BOOLEAN
('not' (All ((Ex (a,B,G)),A,G))) . z is boolean Element of BOOLEAN
(Ex ((Ex (a,A,G)),B,G)) . z is boolean Element of BOOLEAN
'not' ((Ex ((Ex (a,A,G)),B,G)) . z) is boolean Element of BOOLEAN
K105(1,((Ex ((Ex (a,A,G)),B,G)) . z)) is set
CompF (B,G) is non empty with_non-empty_elements a_partition of Y
EqClass (z,(CompF (B,G))) is Element of CompF (B,G)
B_SUP ((Ex (a,A,G)),(CompF (B,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(B_SUP ((Ex (a,A,G)),(CompF (B,G)))) . z is boolean Element of BOOLEAN
x is Element of Y
(Ex (a,A,G)) . x is boolean Element of BOOLEAN
CompF (A,G) is non empty with_non-empty_elements a_partition of Y
B_SUP (a,(CompF (A,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
x is Element of Y
EqClass (x,(CompF (A,G))) is Element of CompF (A,G)
(Ex (a,A,G)) . x is boolean Element of BOOLEAN
SS is Element of Y
a . SS is boolean Element of BOOLEAN
x is Element of Y
a . x is boolean Element of BOOLEAN
EqClass (x,(CompF (A,G))) is Element of CompF (A,G)
B_SUP (a,(CompF (B,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(B_SUP (a,(CompF (B,G)))) . z is boolean Element of BOOLEAN
EqClass (z,(CompF (A,G))) is Element of CompF (A,G)
(Ex (a,B,G)) . z is boolean Element of BOOLEAN
B_INF ((Ex (a,B,G)),(CompF (A,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(B_INF ((Ex (a,B,G)),(CompF (A,G)))) . z is boolean Element of BOOLEAN
(All ((Ex (a,B,G)),A,G)) . z is boolean Element of BOOLEAN
'not' ((All ((Ex (a,B,G)),A,G)) . z) is boolean Element of BOOLEAN
K105(1,((All ((Ex (a,B,G)),A,G)) . z)) is set
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (All (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (All (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (Ex (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (Ex (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (Ex (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (Ex (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
z is Element of Y
(All (('not' (Ex (a,A,G))),B,G)) . z is boolean Element of BOOLEAN
('not' (Ex ((All (a,B,G)),A,G))) . z is boolean Element of BOOLEAN
CompF (B,G) is non empty with_non-empty_elements a_partition of Y
B_INF (('not' (Ex (a,A,G))),(CompF (B,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
EqClass (z,(CompF (B,G))) is Element of CompF (B,G)
('not' (Ex (a,A,G))) . z is boolean Element of BOOLEAN
CompF (A,G) is non empty with_non-empty_elements a_partition of Y
B_SUP (a,(CompF (A,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(Ex (a,A,G)) . z is boolean Element of BOOLEAN
'not' ((Ex (a,A,G)) . z) is boolean Element of BOOLEAN
K105(1,((Ex (a,A,G)) . z)) is set
B_INF (a,(CompF (B,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
EqClass (z,(CompF (A,G))) is Element of CompF (A,G)
x is Element of Y
(All (a,B,G)) . x is boolean Element of BOOLEAN
a . x is boolean Element of BOOLEAN
EqClass (x,(CompF (B,G))) is Element of CompF (B,G)
B_SUP ((All (a,B,G)),(CompF (A,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
(B_SUP ((All (a,B,G)),(CompF (A,G)))) . z is boolean Element of BOOLEAN
(Ex ((All (a,B,G)),A,G)) . z is boolean Element of BOOLEAN
'not' ((Ex ((All (a,B,G)),A,G)) . z) is boolean Element of BOOLEAN
K105(1,((Ex ((All (a,B,G)),A,G)) . z)) is set
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex (('not' (All (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All (('not' (All (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (Ex (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (Ex (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((Ex (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((Ex (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' (Ex (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' (Ex (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((All (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
Ex (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
All ((Ex (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (Ex ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Y is non empty set
[:Y,BOOLEAN:] is set
bool [:Y,BOOLEAN:] is set
PARTITIONS Y is partition-membered Element of bool (bool (bool Y))
bool Y is Element of bool (bool Y)
bool Y is set
bool (bool Y) is set
bool (bool Y) is set
bool (bool (bool Y)) is set
bool (PARTITIONS Y) is set
a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
G is Element of bool (PARTITIONS Y)
A is non empty with_non-empty_elements a_partition of Y
All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
B is non empty with_non-empty_elements a_partition of Y
Ex ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]
'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]