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