:: BVFUNC11 semantic presentation

K128() is Element of bool K124()

K124() is set

bool K124() is set

K123() is set

bool K123() is set

bool K128() is set

BOOLEAN is non empty set

{} is empty V56() set

the empty V56() set is empty V56() set

{{}} is non empty set

TRUE is boolean Element of BOOLEAN

1 is non empty set

FALSE is boolean Element of BOOLEAN

K129() is empty V56() Element of K128()

K174() is set

K175() is set

Y is non empty set

a is Element of Y

G is non empty with_non-empty_elements a_partition of Y

A is non empty with_non-empty_elements a_partition of Y

EqClass (a,G) is Element of G

EqClass (a,A) is Element of A

B is set

Y is non empty set

a is Element of Y

G is non empty with_non-empty_elements a_partition of Y

EqClass (a,G) is Element of G

A is non empty with_non-empty_elements a_partition of Y

G '\/' A is non empty with_non-empty_elements a_partition of Y

EqClass (a,(G '\/' A)) is Element of G '\/' A

Y is non empty set

a is Element of Y

G is non empty with_non-empty_elements a_partition of Y

A is non empty with_non-empty_elements a_partition of Y

G '/\' A is non empty with_non-empty_elements a_partition of Y

EqClass (a,(G '/\' A)) is Element of G '/\' A

EqClass (a,G) is Element of G

Y is non empty set

A is non empty set

a is Element of Y

G is non empty with_non-empty_elements a_partition of Y

EqClass (a,G) is Element of G

%O Y is non empty with_non-empty_elements a_partition of Y

EqClass (a,(%O Y)) is Element of %O Y

B is Element of A

SmallestPartition A is non empty with_non-empty_elements a_partition of A

EqClass (B,(SmallestPartition A)) is Element of SmallestPartition A

z is non empty with_non-empty_elements a_partition of A

EqClass (B,z) is Element of z

Y is non empty set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Element of bool (PARTITIONS Y)

G is non empty with_non-empty_elements a_partition of Y

A is non empty with_non-empty_elements a_partition of Y

{G,A} is non empty set

B is set

z is set

(G,A) --> (B,z) is Relation-like Function-like set

SS is set

((G,A) --> (B,z)) . SS is set

{B,z} is non empty set

SS is set

dom ((G,A) --> (B,z)) is set

rng ((G,A) --> (B,z)) is set

SS is Element of bool (bool Y)

Intersect SS is Element of bool Y

B /\ z is set

Y is non empty set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Element of bool (PARTITIONS Y)

'/\' a is non empty with_non-empty_elements a_partition of Y

G is non empty with_non-empty_elements a_partition of Y

A is non empty with_non-empty_elements a_partition of Y

{G,A} is non empty set

G '/\' A is non empty with_non-empty_elements a_partition of Y

B is set

z is Relation-like Function-like set

dom z is set

rng z is set

x is Element of bool (bool Y)

Intersect x is Element of bool Y

z . G is set

meet (rng z) is set

z . A is set

(z . G) /\ (z . A) is set

{(z . G),(z . A)} is non empty set

SS is set

h is set

z . h is set

SS is set

SS is set

h is set

SS is set

INTERSECTION (G,A) is set

(INTERSECTION (G,A)) \ {{}} is Element of bool (INTERSECTION (G,A))

bool (INTERSECTION (G,A)) is set

B is set

INTERSECTION (G,A) is set

(INTERSECTION (G,A)) \ {{}} is Element of bool (INTERSECTION (G,A))

bool (INTERSECTION (G,A)) is set

z is set

x is set

z /\ x is set

{z,x} is non empty set

SS is set

SS is Element of bool (bool Y)

Intersect SS is Element of bool Y

(G,A) --> (z,x) is Relation-like Function-like set

d is set

((G,A) --> (z,x)) . d is set

dom ((G,A) --> (z,x)) is set

rng ((G,A) --> (z,x)) is set

Y is non empty set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Element of bool (PARTITIONS Y)

G is non empty with_non-empty_elements a_partition of Y

A is non empty with_non-empty_elements a_partition of Y

{G,A} is non empty set

CompF (G,a) is non empty with_non-empty_elements a_partition of Y

{A} is non empty Element of bool (PARTITIONS Y)

'/\' {A} is non empty with_non-empty_elements a_partition of Y

B is set

z is Relation-like Function-like set

dom z is set

rng z is set

x is Element of bool (bool Y)

Intersect x is Element of bool Y

z . A is set

{(z . A)} is non empty set

meet {(z . A)} is set

B is set

A .--> B is trivial Relation-like {A} -defined Function-like one-to-one set

{A} is non empty set

{A} --> B is non empty Relation-like {A} -defined Function-like constant V17({A}) quasi_total Element of bool [:{A},{B}:]

{B} is non empty set

[:{A},{B}:] is set

bool [:{A},{B}:] is set

dom (A .--> B) is set

x is set

(A .--> B) . x is set

rng (A .--> B) is set

x is set

x is Element of bool (bool Y)

meet x is Element of bool Y

Intersect x is Element of bool Y

{G} is non empty Element of bool (PARTITIONS Y)

{G} \ {G} is Element of bool (PARTITIONS Y)

a \ {G} is Element of bool (PARTITIONS Y)

{G} \/ {A} is non empty Element of bool (PARTITIONS Y)

({G} \/ {A}) \ {G} is Element of bool (PARTITIONS Y)

{A} \ {G} is Element of bool (PARTITIONS Y)

({G} \ {G}) \/ ({A} \ {G}) is Element of bool (PARTITIONS Y)

({G} \ {G}) \/ {A} is non empty Element of bool (PARTITIONS Y)

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

A is Element of bool (PARTITIONS Y)

B is non empty with_non-empty_elements a_partition of Y

All (a,B,A) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (G,B,A) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (G,B,A) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

CompF (B,G) is non empty with_non-empty_elements a_partition of Y

B_SUP (a,(CompF (B,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

z is Element of Y

(All ((Ex (a,A,G)),B,G)) . z is boolean Element of BOOLEAN

(Ex ((Ex (a,B,G)),A,G)) . z is boolean Element of BOOLEAN

EqClass (z,(CompF (B,G))) is Element of CompF (B,G)

B_INF ((Ex (a,A,G)),(CompF (B,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

(B_INF ((Ex (a,A,G)),(CompF (B,G)))) . z is boolean Element of BOOLEAN

x is Element of Y

(Ex (a,A,G)) . x is boolean Element of BOOLEAN

CompF (A,G) is non empty with_non-empty_elements a_partition of Y

EqClass (z,(CompF (A,G))) is Element of CompF (A,G)

B_SUP (a,(CompF (A,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

(B_SUP (a,(CompF (A,G)))) . z is boolean Element of BOOLEAN

(Ex (a,A,G)) . z is boolean Element of BOOLEAN

x is Element of Y

a . x is boolean Element of BOOLEAN

x is Element of Y

a . x is boolean Element of BOOLEAN

EqClass (x,(CompF (B,G))) is Element of CompF (B,G)

(Ex (a,B,G)) . x is boolean Element of BOOLEAN

B_SUP ((Ex (a,B,G)),(CompF (A,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

(B_SUP ((Ex (a,B,G)),(CompF (A,G)))) . z is boolean Element of BOOLEAN

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

CompF (A,G) is non empty with_non-empty_elements a_partition of Y

B_INF (a,(CompF (A,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

z is Element of Y

('not' (Ex ((All (a,A,G)),B,G))) . z is boolean Element of BOOLEAN

(Ex ((Ex (('not' a),B,G)),A,G)) . z is boolean Element of BOOLEAN

CompF (B,G) is non empty with_non-empty_elements a_partition of Y

EqClass (z,(CompF (B,G))) is Element of CompF (B,G)

(Ex ((All (a,A,G)),B,G)) . z is boolean Element of BOOLEAN

'not' ((Ex ((All (a,A,G)),B,G)) . z) is boolean Element of BOOLEAN

K105(1,((Ex ((All (a,A,G)),B,G)) . z)) is set

B_SUP ((All (a,A,G)),(CompF (B,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

(All (a,A,G)) . z is boolean Element of BOOLEAN

EqClass (z,(CompF (A,G))) is Element of CompF (A,G)

x is Element of Y

a . x is boolean Element of BOOLEAN

('not' a) . x is boolean Element of BOOLEAN

'not' FALSE is boolean Element of BOOLEAN

K105(1,FALSE) is set

B_SUP (('not' a),(CompF (B,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

EqClass (x,(CompF (B,G))) is Element of CompF (B,G)

(Ex (('not' a),B,G)) . x is boolean Element of BOOLEAN

B_SUP ((Ex (('not' a),B,G)),(CompF (A,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

(B_SUP ((Ex (('not' a),B,G)),(CompF (A,G)))) . z is boolean Element of BOOLEAN

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

Ex (('not' (All (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((Ex (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All (('not' (All (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((Ex (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((Ex (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((Ex (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (('not' (All (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((Ex (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' (All (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All (('not' (All (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

z is Element of Y

(All ((All (('not' a),A,G)),B,G)) . z is boolean Element of BOOLEAN

('not' (All ((All (a,B,G)),A,G))) . z is boolean Element of BOOLEAN

CompF (A,G) is non empty with_non-empty_elements a_partition of Y

EqClass (z,(CompF (A,G))) is Element of CompF (A,G)

CompF (B,G) is non empty with_non-empty_elements a_partition of Y

EqClass (z,(CompF (B,G))) is Element of CompF (B,G)

B_INF ((All (('not' a),A,G)),(CompF (B,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

(B_INF ((All (('not' a),A,G)),(CompF (B,G)))) . z is boolean Element of BOOLEAN

x is Element of Y

(All (('not' a),A,G)) . x is boolean Element of BOOLEAN

B_INF (('not' a),(CompF (A,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

(All (('not' a),A,G)) . z is boolean Element of BOOLEAN

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

a . z is boolean Element of BOOLEAN

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

K105(1,(a . z)) is set

B_INF (a,(CompF (B,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

(B_INF (a,(CompF (B,G)))) . z is boolean Element of BOOLEAN

(All (a,B,G)) . z is boolean Element of BOOLEAN

B_INF ((All (a,B,G)),(CompF (A,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

(B_INF ((All (a,B,G)),(CompF (A,G)))) . z is boolean Element of BOOLEAN

(All ((All (a,B,G)),A,G)) . z is boolean Element of BOOLEAN

'not' ((All ((All (a,B,G)),A,G)) . z) is boolean Element of BOOLEAN

K105(1,((All ((All (a,B,G)),A,G)) . z)) is set

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((Ex (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

Ex ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

Ex (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

G is Element of bool (PARTITIONS Y)

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((Ex (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

z is Element of Y

('not' (Ex ((Ex (a,A,G)),B,G))) . z is boolean Element of BOOLEAN

('not' (All ((Ex (a,B,G)),A,G))) . z is boolean Element of BOOLEAN

(Ex ((Ex (a,A,G)),B,G)) . z is boolean Element of BOOLEAN

'not' ((Ex ((Ex (a,A,G)),B,G)) . z) is boolean Element of BOOLEAN

K105(1,((Ex ((Ex (a,A,G)),B,G)) . z)) is set

CompF (B,G) is non empty with_non-empty_elements a_partition of Y

EqClass (z,(CompF (B,G))) is Element of CompF (B,G)

B_SUP ((Ex (a,A,G)),(CompF (B,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

(B_SUP ((Ex (a,A,G)),(CompF (B,G)))) . z is boolean Element of BOOLEAN

x is Element of Y

(Ex (a,A,G)) . x is boolean Element of BOOLEAN

CompF (A,G) is non empty with_non-empty_elements a_partition of Y

B_SUP (a,(CompF (A,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

x is Element of Y

EqClass (x,(CompF (A,G))) is Element of CompF (A,G)

(Ex (a,A,G)) . x is boolean Element of BOOLEAN

SS is Element of Y

a . SS is boolean Element of BOOLEAN

x is Element of Y

a . x is boolean Element of BOOLEAN

EqClass (x,(CompF (A,G))) is Element of CompF (A,G)

B_SUP (a,(CompF (B,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

(B_SUP (a,(CompF (B,G)))) . z is boolean Element of BOOLEAN

EqClass (z,(CompF (A,G))) is Element of CompF (A,G)

(Ex (a,B,G)) . z is boolean Element of BOOLEAN

B_INF ((Ex (a,B,G)),(CompF (A,G))) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

(B_INF ((Ex (a,B,G)),(CompF (A,G)))) . z is boolean Element of BOOLEAN

(All ((Ex (a,B,G)),A,G)) . z is boolean Element of BOOLEAN

'not' ((All ((Ex (a,B,G)),A,G)) . z) is boolean Element of BOOLEAN

K105(1,((All ((Ex (a,B,G)),A,G)) . z)) is set

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (('not' (All (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

All (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

Ex ((All (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((All (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (('not' (All (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (('not' a),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((All (('not' a),A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex (a,A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (('not' (Ex (a,A,G))),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((All (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((All (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' (Ex (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((Ex (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((All (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (('not' (Ex (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((Ex (a,B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((Ex (a,B,G)),A,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

Ex ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (Ex ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

B is non empty with_non-empty_elements a_partition of Y

All ((Ex (a,A,G)),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All ((Ex (a,A,G)),B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Ex (('not' a),B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All ((Ex (('not' a),B,G)),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (a,B,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' (All (a,B,G)) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

All (('not' (All (a,B,G))),A,G) is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

Y is non empty set

[:Y,BOOLEAN:] is set

bool [:Y,BOOLEAN:] is set

PARTITIONS Y is partition-membered Element of bool (bool (bool Y))

bool Y is Element of bool (bool Y)

bool Y is set

bool (bool Y) is set

bool (bool Y) is set

bool (bool (bool Y)) is set

bool (PARTITIONS Y) is set

a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

'not' a is Function-like quasi_total boolean-valued Element of bool [:Y,BOOLEAN:]

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

Ex (a,A,G) is Function-like quasi_total boolean-valued Element of bool