:: BVFUNC14 semantic presentation

K129() is Element of bool K125()

K125() is set

bool K125() is non empty set

K124() is set

bool K124() is non empty set

bool K129() is non empty set

K211() is set

{} is empty set

{{}} is non empty set

Y is non empty set

G is Element of Y

A is non empty with_non-empty_elements a_partition of Y

B is non empty with_non-empty_elements a_partition of Y

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

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

EqClass (G,A) is Element of A

EqClass (G,B) is Element of B

(EqClass (G,A)) /\ (EqClass (G,B)) is Element of bool Y

bool Y is non empty set

D is set

E is Element of Y

EqClass (E,A) is Element of A

EqClass (E,B) is Element of B

INTERSECTION (A,B) is set

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

bool (INTERSECTION (A,B)) is non empty set

F is set

J is set

F /\ J is set

(EqClass (E,A)) /\ (EqClass (E,B)) is Element of bool Y

C is set

Y is non empty set

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

bool Y is non empty Element of bool (bool Y)

bool Y is non empty set

bool (bool Y) is non empty set

bool (bool Y) is non empty set

bool (bool (bool Y)) is non empty set

bool (PARTITIONS Y) is non empty set

G 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

B is non empty with_non-empty_elements a_partition of Y

{A,B} is non empty set

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

C is set

INTERSECTION (A,B) is set

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

bool (INTERSECTION (A,B)) is non empty set

D is set

E is set

D /\ E is set

(A,B) --> (D,E) is Relation-like bool (bool Y) -defined Function-like set

rng ((A,B) --> (D,E)) is set

{D,E} is non empty set

J is set

J is Element of bool (bool Y)

Intersect J is Element of bool Y

M is set

N is set

meet J is Element of bool Y

M is set

((A,B) --> (D,E)) . M is set

M is set

meet J is Element of bool Y

dom ((A,B) --> (D,E)) is set

C is set

D is Relation-like Function-like set

dom D is set

rng D is set

E is Element of bool (bool Y)

Intersect E is Element of bool Y

D . A is set

D . B is set

(D . A) /\ (D . B) is set

F is set

{(D . A),(D . B)} is non empty set

J is set

M is set

D . M is set

J is set

meet (rng D) is set

F is set

meet (rng D) is set

INTERSECTION (A,B) is set

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

bool (INTERSECTION (A,B)) is non empty set

Y is set

B is set

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

{Y} is non empty set

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

{B} is non empty set

[:{Y},{B}:] is non empty set

bool [:{Y},{B}:] is non empty set

G is set

C is set

G .--> C is trivial Relation-like {G} -defined Function-like one-to-one set

{G} is non empty set

{G} --> C is non empty Relation-like {G} -defined Function-like constant V17({G}) V21({G},{C}) Element of bool [:{G},{C}:]

{C} is non empty set

[:{G},{C}:] is non empty set

bool [:{G},{C}:] is non empty set

(Y .--> B) +* (G .--> C) is Relation-like Function-like set

A is set

D is set

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

{A} is non empty set

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

{D} is non empty set

[:{A},{D}:] is non empty set

bool [:{A},{D}:] is non empty set

((Y .--> B) +* (G .--> C)) +* (A .--> D) is Relation-like Function-like set

dom (((Y .--> B) +* (G .--> C)) +* (A .--> D)) is set

{Y,G,A} is non empty set

dom (G .--> C) is set

dom (A .--> D) is set

dom ((Y .--> B) +* (G .--> C)) is set

dom (Y .--> B) is set

(dom (Y .--> B)) \/ (dom (G .--> C)) is set

{Y} \/ {G} is non empty set

({Y} \/ {G}) \/ {A} is non empty set

{Y,G} is non empty set

{Y,G} \/ {A} is non empty set

Y is Relation-like Function-like set

G is set

A is set

B is set

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

{G} is non empty set

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

{B} is non empty set

[:{G},{B}:] is non empty set

bool [:{G},{B}:] is non empty set

Y +* (G .--> B) is Relation-like Function-like set

C is set

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

{A} is non empty set

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

{C} is non empty set

[:{A},{C}:] is non empty set

bool [:{A},{C}:] is non empty set

(Y +* (G .--> B)) +* (A .--> C) is Relation-like Function-like set

((Y +* (G .--> B)) +* (A .--> C)) . G is set

dom (A .--> C) is set

(Y +* (G .--> B)) . G is set

dom (G .--> B) is set

(G .--> B) . G is set

Y is set

G is set

A is set

B is set

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

{Y} is non empty set

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

{B} is non empty set

[:{Y},{B}:] is non empty set

bool [:{Y},{B}:] is non empty set

C is set

G .--> C is trivial Relation-like {G} -defined Function-like one-to-one set

{G} is non empty set

{G} --> C is non empty Relation-like {G} -defined Function-like constant V17({G}) V21({G},{C}) Element of bool [:{G},{C}:]

{C} is non empty set

[:{G},{C}:] is non empty set

bool [:{G},{C}:] is non empty set

(Y .--> B) +* (G .--> C) is Relation-like Function-like set

D is set

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

{A} is non empty set

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

{D} is non empty set

[:{A},{D}:] is non empty set

bool [:{A},{D}:] is non empty set

((Y .--> B) +* (G .--> C)) +* (A .--> D) is Relation-like Function-like set

(((Y .--> B) +* (G .--> C)) +* (A .--> D)) . Y is set

dom (A .--> D) is set

((Y .--> B) +* (G .--> C)) . Y is set

dom (G .--> C) is set

(Y .--> B) . Y is set

Y is set

B is set

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

{Y} is non empty set

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

{B} is non empty set

[:{Y},{B}:] is non empty set

bool [:{Y},{B}:] is non empty set

G is set

C is set

G .--> C is trivial Relation-like {G} -defined Function-like one-to-one set

{G} is non empty set

{G} --> C is non empty Relation-like {G} -defined Function-like constant V17({G}) V21({G},{C}) Element of bool [:{G},{C}:]

{C} is non empty set

[:{G},{C}:] is non empty set

bool [:{G},{C}:] is non empty set

(Y .--> B) +* (G .--> C) is Relation-like Function-like set

A is set

D is set

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

{A} is non empty set

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

{D} is non empty set

[:{A},{D}:] is non empty set

bool [:{A},{D}:] is non empty set

((Y .--> B) +* (G .--> C)) +* (A .--> D) is Relation-like Function-like set

E is Relation-like Function-like set

rng E is set

E . Y is set

E . G is set

E . A is set

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

dom E is set

{Y,G,A} is non empty set

F is set

J is set

E . J is set

F is set

Y is non empty set

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

bool Y is non empty Element of bool (bool Y)

bool Y is non empty set

bool (bool Y) is non empty set

bool (bool Y) is non empty set

bool (bool (bool Y)) is non empty set

bool (PARTITIONS Y) is non empty set

G 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

B is non empty with_non-empty_elements a_partition of Y

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

C is non empty with_non-empty_elements a_partition of Y

{A,B,C} is non empty set

(A '/\' B) '/\' C is non empty with_non-empty_elements a_partition of Y

D is set

INTERSECTION ((A '/\' B),C) is set

(INTERSECTION ((A '/\' B),C)) \ {{}} is Element of bool (INTERSECTION ((A '/\' B),C))

bool (INTERSECTION ((A '/\' B),C)) is non empty set

E is set

F is set

E /\ F is set

INTERSECTION (A,B) is set

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

bool (INTERSECTION (A,B)) is non empty set

J is set

M is set

J /\ M is set

A .--> J is trivial Relation-like {A} -defined bool (bool Y) -defined {A} -defined Function-like one-to-one set

{A} is non empty set

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

{J} is non empty set

[:{A},{J}:] is non empty set

bool [:{A},{J}:] is non empty set

B .--> M is trivial Relation-like {B} -defined bool (bool Y) -defined {B} -defined Function-like one-to-one set

{B} is non empty set

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

{M} is non empty set

[:{B},{M}:] is non empty set

bool [:{B},{M}:] is non empty set

(A .--> J) +* (B .--> M) is Relation-like bool (bool Y) -defined Function-like set

C .--> F is trivial Relation-like {C} -defined bool (bool Y) -defined {C} -defined Function-like one-to-one set

{C} is non empty set

{C} --> F is non empty Relation-like {C} -defined Function-like constant V17({C}) V21({C},{F}) Element of bool [:{C},{F}:]

{F} is non empty set

[:{C},{F}:] is non empty set

bool [:{C},{F}:] is non empty set

((A .--> J) +* (B .--> M)) +* (C .--> F) is Relation-like bool (bool Y) -defined Function-like set

rng (((A .--> J) +* (B .--> M)) +* (C .--> F)) is set

(((A .--> J) +* (B .--> M)) +* (C .--> F)) . A is set

(((A .--> J) +* (B .--> M)) +* (C .--> F)) . B is set

(((A .--> J) +* (B .--> M)) +* (C .--> F)) . C is set

{((((A .--> J) +* (B .--> M)) +* (C .--> F)) . A),((((A .--> J) +* (B .--> M)) +* (C .--> F)) . B),((((A .--> J) +* (B .--> M)) +* (C .--> F)) . C)} is non empty set

{((((A .--> J) +* (B .--> M)) +* (C .--> F)) . C),((((A .--> J) +* (B .--> M)) +* (C .--> F)) . A),((((A .--> J) +* (B .--> M)) +* (C .--> F)) . B)} is non empty set

z is set

u is set

(((A .--> J) +* (B .--> M)) +* (C .--> F)) . u is set

z is Element of bool (bool Y)

Intersect z is Element of bool Y

u is set

h is set

M /\ F is set

J /\ (M /\ F) is set

J /\ F is set

M /\ (J /\ F) is set

meet z is Element of bool Y

dom (((A .--> J) +* (B .--> M)) +* (C .--> F)) is set

u is set

meet (rng (((A .--> J) +* (B .--> M)) +* (C .--> F))) is set

D is set

E is Relation-like Function-like set

dom E is set

rng E is set

F is Element of bool (bool Y)

Intersect F is Element of bool Y

E . C is set

E . A is set

E . B is set

(E . A) /\ (E . B) is set

((E . A) /\ (E . B)) /\ (E . C) is set

M is set

meet (rng E) is set

INTERSECTION (A,B) is set

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

bool (INTERSECTION (A,B)) is non empty set

M is set

{(E . A),(E . B),(E . C)} is non empty set

N is set

z is set

E . z is set

N is set

meet (rng E) is set

INTERSECTION ((A '/\' B),C) is set

(INTERSECTION ((A '/\' B),C)) \ {{}} is Element of bool (INTERSECTION ((A '/\' B),C))

bool (INTERSECTION ((A '/\' B),C)) is non empty set

Y is non empty set

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

bool Y is non empty Element of bool (bool Y)

bool Y is non empty set

bool (bool Y) is non empty set

bool (bool Y) is non empty set

bool (bool (bool Y)) is non empty set

bool (PARTITIONS Y) is non empty set

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

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

B is non empty with_non-empty_elements a_partition of Y

C is non empty with_non-empty_elements a_partition of Y

{A,B,C} is non empty set

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

{B,C,A} is non empty set

{B,A} is non empty set

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

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

{B,C} is non empty set

{A} \/ {B,C} is non empty set

({A} \/ {B,C}) \ {A} is Element of bool ({A} \/ {B,C})

bool ({A} \/ {B,C}) is non empty set

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

{B,C} \ {A} is Element of bool {B,C}

bool {B,C} is non empty set

({A} \ {A}) \/ ({B,C} \ {A}) is set

({A} \ {A}) \/ {B,C} is non empty set

{} \/ {B,C} is non empty set

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

D is set

E is Relation-like Function-like set

dom E is set

rng E is set

F is Element of bool (bool Y)

Intersect F is Element of bool Y

E . B is set

E . C is set

(E . B) /\ (E . C) is set

J is set

{(E . B),(E . C)} is non empty set

M is set

N is set

E . N is set

M is set

meet (rng E) is set

J is set

meet (rng E) is set

INTERSECTION (B,C) is set

(INTERSECTION (B,C)) \ {{}} is Element of bool (INTERSECTION (B,C))

bool (INTERSECTION (B,C)) is non empty set

D is set

INTERSECTION (B,C) is set

(INTERSECTION (B,C)) \ {{}} is Element of bool (INTERSECTION (B,C))

bool (INTERSECTION (B,C)) is non empty set

E is set

F is set

E /\ F is set

(B,C) --> (E,F) is Relation-like bool (bool Y) -defined Function-like set

dom ((B,C) --> (E,F)) is set

rng ((B,C) --> (E,F)) is set

{E,F} is non empty set

M is set

M is Element of bool (bool Y)

Intersect M is Element of bool Y

N is set

z is set

meet M is Element of bool Y

N is set

((B,C) --> (E,F)) . N is set

N is set

meet M is Element of bool Y

Y is non empty set

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

bool Y is non empty Element of bool (bool Y)

bool Y is non empty set

bool (bool Y) is non empty set

bool (bool Y) is non empty set

bool (bool (bool Y)) is non empty set

bool (PARTITIONS Y) is non empty set

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

B is non empty with_non-empty_elements a_partition of Y

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

C is non empty with_non-empty_elements a_partition of Y

{A,B,C} is non empty set

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

{B,C,A} is non empty set

Y is non empty set

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

bool Y is non empty Element of bool (bool Y)

bool Y is non empty set

bool (bool Y) is non empty set

bool (bool Y) is non empty set

bool (bool (bool Y)) is non empty set

bool (PARTITIONS Y) is non empty set

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

B is non empty with_non-empty_elements a_partition of Y

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

C is non empty with_non-empty_elements a_partition of Y

{A,B,C} is non empty set

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

{C,A,B} is non empty set

Y is non empty set

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

bool Y is non empty Element of bool (bool Y)

bool Y is non empty set

bool (bool Y) is non empty set

bool (bool Y) is non empty set

bool (bool (bool Y)) is non empty set

bool (PARTITIONS Y) is non empty set

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

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

B is non empty with_non-empty_elements a_partition of Y

C is non empty with_non-empty_elements a_partition of Y

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

D is non empty with_non-empty_elements a_partition of Y

{A,B,C,D} is non empty set

(B '/\' C) '/\' D is non empty with_non-empty_elements a_partition of Y

{B,B,A,D} is non empty set

{B,A,D} is non empty set

{A,B,D} is non empty set

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

{B,B,A,C} is non empty set

{B,A,C} is non empty set

{A,B,C} is non empty set

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

(B '/\' D) '/\' C is non empty with_non-empty_elements a_partition of Y

{C,C,A,B} is non empty set

{C,A,B} is non empty set

{A,B,C} is non empty set

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

B '/\' (C '/\' D) is non empty with_non-empty_elements a_partition of Y

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

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

{B,C,D} is non empty set

{A} \/ {B,C,D} is non empty set

({A} \/ {B,C,D}) \ {A} is Element of bool ({A} \/ {B,C,D})

bool ({A} \/ {B,C,D}) is non empty set

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

{B,C,D} \ {A} is Element of bool {B,C,D}

bool {B,C,D} is non empty set

({A} \ {A}) \/ ({B,C,D} \ {A}) is set

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

{C,D} is non empty set

{B} \/ {C,D} is non empty set

({B} \/ {C,D}) \ {A} is Element of bool ({B} \/ {C,D})

bool ({B} \/ {C,D}) is non empty set

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

{C,D} \ {A} is Element of bool {C,D}

bool {C,D} is non empty set

({B} \ {A}) \/ ({C,D} \ {A}) is set

({B} \ {A}) \/ {C,D} is non empty set

{} \/ {B,C,D} is non empty set

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

E is set

INTERSECTION ((B '/\' C),D) is set

(INTERSECTION ((B '/\' C),D)) \ {{}} is Element of bool (INTERSECTION ((B '/\' C),D))

bool (INTERSECTION ((B '/\' C),D)) is non empty set

F is set

J is set

F /\ J is set

INTERSECTION (B,C) is set

(INTERSECTION (B,C)) \ {{}} is Element of bool (INTERSECTION (B,C))

bool (INTERSECTION (B,C)) is non empty set

M is set

N is set

M /\ N is set

B .--> M is trivial Relation-like {B} -defined bool (bool Y) -defined {B} -defined Function-like one-to-one set

{B} is non empty set

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

{M} is non empty set

[:{B},{M}:] is non empty set

bool [:{B},{M}:] is non empty set

C .--> N is trivial Relation-like {C} -defined bool (bool Y) -defined {C} -defined Function-like one-to-one set

{C} is non empty set

{C} --> N is non empty Relation-like {C} -defined Function-like constant V17({C}) V21({C},{N}) Element of bool [:{C},{N}:]

{N} is non empty set

[:{C},{N}:] is non empty set

bool [:{C},{N}:] is non empty set

(B .--> M) +* (C .--> N) is Relation-like bool (bool Y) -defined Function-like set

D .--> J is trivial Relation-like {D} -defined bool (bool Y) -defined {D} -defined Function-like one-to-one set

{D} is non empty set

{D} --> J is non empty Relation-like {D} -defined Function-like constant V17({D}) V21({D},{J}) Element of bool [:{D},{J}:]

{J} is non empty set

[:{D},{J}:] is non empty set

bool [:{D},{J}:] is non empty set

((B .--> M) +* (C .--> N)) +* (D .--> J) is Relation-like bool (bool Y) -defined Function-like set

(((B .--> M) +* (C .--> N)) +* (D .--> J)) . D is set

(((B .--> M) +* (C .--> N)) +* (D .--> J)) . C is set

rng (((B .--> M) +* (C .--> N)) +* (D .--> J)) is set

(((B .--> M) +* (C .--> N)) +* (D .--> J)) . B is set

{((((B .--> M) +* (C .--> N)) +* (D .--> J)) . B),((((B .--> M) +* (C .--> N)) +* (D .--> J)) . C),((((B .--> M) +* (C .--> N)) +* (D .--> J)) . D)} is non empty set

{((((B .--> M) +* (C .--> N)) +* (D .--> J)) . D),((((B .--> M) +* (C .--> N)) +* (D .--> J)) . B),((((B .--> M) +* (C .--> N)) +* (D .--> J)) . C)} is non empty set

u is set

u is Element of bool (bool Y)

Intersect u is Element of bool Y

h is set

L is set

N /\ J is set

M /\ (N /\ J) is set

M /\ J is set

N /\ (M /\ J) is set

meet u is Element of bool Y

h is set

(((B .--> M) +* (C .--> N)) +* (D .--> J)) . h is set

dom (((B .--> M) +* (C .--> N)) +* (D .--> J)) is set

h is set

meet (rng (((B .--> M) +* (C .--> N)) +* (D .--> J))) is set

E is set

F is Relation-like Function-like set

dom F is set

rng F is set

J is Element of bool (bool Y)

Intersect J is Element of bool Y

F . D is set

F . B is set

F . C is set

(F . B) /\ (F . C) is set

((F . B) /\ (F . C)) /\ (F . D) is set

N is set

meet (rng F) is set

INTERSECTION (B,C) is set

(INTERSECTION (B,C)) \ {{}} is Element of bool (INTERSECTION (B,C))

bool (INTERSECTION (B,C)) is non empty set

N is set

{(F . B),(F . C),(F . D)} is non empty set

z is set

u is set

F . u is set

z is set

meet (rng F) is set

INTERSECTION ((B '/\' C),D) is set

(INTERSECTION ((B '/\' C),D)) \ {{}} is Element of bool (INTERSECTION ((B '/\' C),D))

bool (INTERSECTION ((B '/\' C),D)) is non empty set

Y is non empty set

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

bool Y is non empty Element of bool (bool Y)

bool Y is non empty set

bool (bool Y) is non empty set

bool (bool Y) is non empty set

bool (bool (bool Y)) is non empty set

bool (PARTITIONS Y) is non empty set

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

B is non empty with_non-empty_elements a_partition of Y

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

C is non empty with_non-empty_elements a_partition of Y

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

D is non empty with_non-empty_elements a_partition of Y

{A,B,C,D} is non empty set

(A '/\' C) '/\' D is non empty with_non-empty_elements a_partition of Y

{B,A,C,D} is non empty set

Y is non empty set

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

bool Y is non empty Element of bool (bool Y)

bool Y is non empty set

bool (bool Y) is non empty set

bool (bool Y) is non empty set

bool (bool (bool Y)) is non empty set

bool (PARTITIONS Y) is non empty set

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

B is non empty with_non-empty_elements a_partition of Y

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

C is non empty with_non-empty_elements a_partition of Y

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

D is non empty with_non-empty_elements a_partition of Y

{A,B,C,D} is non empty set

(A '/\' B) '/\' D is non empty with_non-empty_elements a_partition of Y

{C,A,B,D} is non empty set

Y is non empty set

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

bool Y is non empty Element of bool (bool Y)

bool Y is non empty set

bool (bool Y) is non empty set

bool (bool Y) is non empty set

bool (bool (bool Y)) is non empty set

bool (PARTITIONS Y) is non empty set

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

B is non empty with_non-empty_elements a_partition of Y

C is non empty with_non-empty_elements a_partition of Y

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

(A '/\' C) '/\' B is non empty with_non-empty_elements a_partition of Y

D is non empty with_non-empty_elements a_partition of Y

{A,B,C,D} is non empty set

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

{D,A,C,B} is non empty set

Y is set

B is set

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

{Y} is non empty set

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

{B} is non empty set

[:{Y},{B}:] is non empty set

bool [:{Y},{B}:] is non empty set

G is set

C is set

G .--> C is trivial Relation-like {G} -defined Function-like one-to-one set

{G} is non empty set

{G} --> C is non empty Relation-like {G} -defined Function-like constant V17({G}) V21({G},{C}) Element of bool [:{G},{C}:]

{C} is non empty set

[:{G},{C}:] is non empty set

bool [:{G},{C}:] is non empty set

(Y .--> B) +* (G .--> C) is Relation-like Function-like set

A is set

D is set

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

{A} is non empty set

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

{D} is non empty set

[:{A},{D}:] is non empty set

bool [:{A},{D}:] is non empty set

((Y .--> B) +* (G .--> C)) +* (A .--> D) is Relation-like Function-like set

dom (((Y .--> B) +* (G .--> C)) +* (A .--> D)) is set

{Y,G,A} is non empty set

G is set

A is set

Y is Relation-like Function-like set

B is set

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

{G} is non empty set

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

{B} is non empty set

[:{G},{B}:] is non empty set

bool [:{G},{B}:] is non empty set

Y +* (G .--> B) is Relation-like Function-like set

C is set

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

{A} is non empty set

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

{C} is non empty set

[:{A},{C}:] is non empty set

bool [:{A},{C}:] is non empty set

(Y +* (G .--> B)) +* (A .--> C) is Relation-like Function-like set

((Y +* (G .--> B)) +* (A .--> C)) . G is set

Y is set

G is set

A is set

B is set

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

{Y} is non empty set

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

{B} is non empty set

[:{Y},{B}:] is non empty set

bool [:{Y},{B}:] is non empty set

C is set

G .--> C is trivial Relation-like {G} -defined Function-like one-to-one set

{G} is non empty set

{G} --> C is non empty Relation-like {G} -defined Function-like constant V17({G}) V21({G},{C}) Element of bool [:{G},{C}:]

{C} is non empty set

[:{G},{C}:] is non empty set

bool [:{G},{C}:] is non empty set

(Y .--> B) +* (G .--> C) is Relation-like Function-like set

D is set

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

{A} is non empty set

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

{D} is non empty set

[:{A},{D}:] is non empty set

bool [:{A},{D}:] is non empty set

((Y .--> B) +* (G .--> C)) +* (A .--> D) is Relation-like Function-like set

(((Y .--> B) +* (G .--> C)) +* (A .--> D)) . Y is set

E is Relation-like Function-like set

Y is set

B is set

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

{Y} is non empty set

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

{B} is non empty set

[:{Y},{B}:] is non empty set

bool [:{Y},{B}:] is non empty set

G is set

C is set

G .--> C is trivial Relation-like {G} -defined Function-like one-to-one set

{G} is non empty set

{G} --> C is non empty Relation-like {G} -defined Function-like constant V17({G}) V21({G},{C}) Element of bool [:{G},{C}:]

{C} is non empty set

[:{G},{C}:] is non empty set

bool [:{G},{C}:] is non empty set

(Y .--> B) +* (G .--> C) is Relation-like Function-like set

A is set

D is set

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

{A} is non empty set

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

{D} is non empty set

[:{A},{D}:] is non empty set

bool [:{A},{D}:] is non empty set

((Y .--> B) +* (G .--> C)) +* (A .--> D) is Relation-like Function-like set

rng E is set

E . Y is set

E . G is set

E . A is set

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

Y is non empty set

G is non empty with_non-empty_elements a_partition of Y

A is non empty with_non-empty_elements a_partition of Y

B is non empty with_non-empty_elements a_partition of Y

C is non empty with_non-empty_elements a_partition of Y

D is Relation-like Function-like set

D . A is set

D . B is set

D . C is set

F is set

A .--> F is trivial Relation-like {A} -defined bool (bool Y) -defined {A} -defined Function-like one-to-one set

{A} is non empty set

bool Y is non empty set

bool (bool Y) is non empty set

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

{F} is non empty set

[:{A},{F}:] is non empty set

bool [:{A},{F}:] is non empty set

J is set

B .--> J is trivial Relation-like {B} -defined bool (bool Y) -defined {B} -defined Function-like one-to-one set

{B} is non empty set

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

{J} is non empty set

[:{B},{J}:] is non empty set

bool [:{B},{J}:] is non empty set

(A .--> F) +* (B .--> J) is Relation-like bool (bool Y) -defined Function-like set

M is set

C .--> M is trivial Relation-like {C} -defined bool (bool Y) -defined {C} -defined Function-like one-to-one set

{C} is non empty set

{C} --> M is non empty Relation-like {C} -defined Function-like constant V17({C}) V21({C},{M}) Element of bool [:{C},{M}:]

{M} is non empty set

[:{C},{M}:] is non empty set

bool [:{C},{M}:] is non empty set

((A .--> F) +* (B .--> J)) +* (C .--> M) is Relation-like bool (bool Y) -defined Function-like set

E is set

G .--> E is trivial Relation-like {G} -defined bool (bool Y) -defined {G} -defined Function-like one-to-one set

{G} is non empty set

{G} --> E is non empty Relation-like {G} -defined Function-like constant V17({G}) V21({G},{E}) Element of bool [:{G},{E}:]

{E} is non empty set

[:{G},{E}:] is non empty set

bool [:{G},{E}:] is non empty set

(((A .--> F) +* (B .--> J)) +* (C .--> M)) +* (G .--> E) is Relation-like bool (bool Y) -defined Function-like set

dom (G .--> E) is set

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

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

bool Y is non empty Element of bool (bool Y)

bool (bool Y) is non empty set

bool (bool (bool Y)) is non empty set

bool (PARTITIONS Y) is non empty set

(((A .--> F) +* (B .--> J)) +* (C .--> M)) . C is set

(((A .--> F) +* (B .--> J)) +* (C .--> M)) . B is set

dom (C .--> M) is set

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

((A .--> F) +* (B .--> J)) . B is set

(((A .--> F) +* (B .--> J)) +* (C .--> M)) . A is set

((A .--> F) +* (B .--> J)) . A is set

dom (B .--> J) is set

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

(A .--> F) . A is set

(B .--> J) . B is set

(C .--> M) . C is set

G is set

A is set

B is set

Y is set

{Y,G,A,B} is non empty set

C is Relation-like Function-like set

dom C is set

E is set

G .--> E is trivial Relation-like {G} -defined Function-like one-to-one set

{G} is non empty set

{G} --> E is non empty Relation-like {G} -defined Function-like constant V17({G}) V21({G},{E}) Element of bool [:{G},{E}:]

{E} is non empty set

[:{G},{E}:] is non empty set

bool [:{G},{E}:] is non empty set

F is set

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

{A} is non empty set

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

{F} is non empty set

[:{A},{F}:] is non empty set

bool [:{A},{F}:] is non empty set

(G .--> E) +* (A .--> F) is Relation-like Function-like set

J is set

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

{B} is non empty set

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

{J} is non empty set

[:{B},{J}:] is non empty set

bool [:{B},{J}:] is non empty set

((G .--> E) +* (A .--> F)) +* (B .--> J) is Relation-like Function-like set

D is set

Y .--> D is trivial Relation-like {Y} -defined Function-like one-to-one set

{Y} is non empty set

{Y} --> D is non empty Relation-like {Y} -defined Function-like constant V17({Y}) V21({Y},{D}) Element of bool [:{Y},{D}:]

{D} is non empty set

[:{Y},{D}:] is non empty set

bool [:{Y},{D}:] is non empty set

(((G .--> E) +* (A .--> F)) +* (B .--> J)) +* (Y .--> D) is Relation-like Function-like set

dom ((G .--> E) +* (A .--> F)) is set

dom (G .--> E) is set

dom (A .--> F) is set

(dom (G .--> E)) \/ (dom (A .--> F)) is set

dom (((G .--> E) +* (A .--> F)) +* (B .--> J)) is set

dom (B .--> J) is set

((dom (G .--> E)) \/ (dom (A .--> F))) \/ (dom (B .--> J)) is set

dom ((((G .--> E) +* (A .--> F)) +* (B .--> J)) +* (Y .--> D)) is set

{G} \/ (dom (A .--> F)) is non empty set

({G} \/ (dom (A .--> F))) \/ (dom (B .--> J)) is non empty set

dom (Y .--> D) is set

(({G} \/ (dom (A .--> F))) \/ (dom (B .--> J))) \/ (dom (Y .--> D)) is non empty set

{G} \/ {A} is non empty set

({G} \/ {A}) \/ (dom (B .--> J)) is non empty set

(({G} \/ {A}) \/ (dom (B .--> J))) \/ (dom (Y .--> D)) is non empty set

({G} \/ {A}) \/ {B} is non empty set

(({G} \/ {A}) \/ {B}) \/ (dom (Y .--> D)) is non empty set

{Y} \/ (({G} \/ {A}) \/ {B}) is non empty set

{G,A} is non empty set

{G,A} \/ {B} is non empty set

{Y} \/ ({G,A} \/ {B}) is non empty set

{G,A,B} is non empty set

{Y} \/ {G,A,B} is non empty set

Y is non empty set

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

bool Y is non empty Element of bool (bool Y)

bool Y is non empty set

bool (bool Y) is non empty set

bool (bool Y) is non empty set

bool (bool (bool Y)) is non empty set

bool (PARTITIONS Y) is non empty set

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

B is non empty with_non-empty_elements a_partition of Y

C is non empty with_non-empty_elements a_partition of Y

D is non empty with_non-empty_elements a_partition of Y

{A,B,C,D} is non empty set

E is Relation-like Function-like set

rng E is set

E . A is set

E . B is set

E . C is set

E . D is set

{(E . A),(E . B),(E . C),(E . D)} is non empty set

J is set

B .--> J is trivial Relation-like {B} -defined bool (bool Y) -defined {B} -defined Function-like one-to-one set

{B} is non empty set

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

{J} is non empty set

[:{B},{J}:] is non empty set

bool [:{B},{J}:] is non empty set

M is set

C .--> M is trivial Relation-like {C} -defined bool (bool Y) -defined {C} -defined Function-like one-to-one set

{C} is non empty set

{C} --> M is non empty Relation-like {C} -defined Function-like constant V17({C}) V21({C},{M}) Element of bool [:{C},{M}:]

{M} is non empty set

[:{C},{M}:] is non empty set

bool [:{C},{M}:] is non empty set

(B .--> J) +* (C .--> M) is Relation-like bool (bool Y) -defined Function-like set

N is set

D .--> N is trivial Relation-like {D} -defined bool (bool Y) -defined {D} -defined Function-like one-to-one set

{D} is non empty set

{D} --> N is non empty Relation-like {D} -defined Function-like constant V17({D}) V21({D},{N}) Element of bool [:{D},{N}:]

{N} is non empty set

[:{D},{N}:] is non empty set

bool [:{D},{N}:] is non empty set

((B .--> J) +* (C .--> M)) +* (D .--> N) is Relation-like bool (bool Y) -defined Function-like set

F is set

A .--> F is trivial Relation-like {A} -defined bool (bool Y) -defined {A} -defined Function-like one-to-one set

{A} is non empty set

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

{F} is non empty set

[:{A},{F}:] is non empty set

bool [:{A},{F}:] is non empty set

(((B .--> J) +* (C .--> M)) +* (D .--> N)) +* (A .--> F) is Relation-like bool (bool Y) -defined Function-like set

dom E is set

z is set

u is set

E . u is set

z is set

Y is non empty set

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

bool Y is non empty Element of bool (bool Y)

bool Y is non empty set

bool (bool Y) is non empty set

bool (bool Y) is non empty set

bool (bool (bool Y)) is non empty set

bool (PARTITIONS Y) is non empty set

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

B is non empty with_non-empty_elements a_partition of Y

C is non empty with_non-empty_elements a_partition of Y

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

D is non empty with_non-empty_elements a_partition of Y

{A,B,C,D} is non empty set

(B '/\' C) '/\' D is non empty with_non-empty_elements a_partition of Y

F is Element of Y

EqClass (F,((B '/\' C) '/\' D)) is Element of (B '/\' C) '/\' D

E is Element of Y

EqClass (E,A) is Element of A

EqClass (F,B) is Element of B

B .--> (EqClass (F,B)) is trivial Relation-like {B} -defined bool (bool Y) -defined {B} -defined B -valued Function-like one-to-one set

{B} is non empty set

{B} --> (EqClass (F,B)) is non empty Relation-like {B} -defined B -valued Function-like constant V17({B}) V21({B},{(EqClass (F,B))}) Element of bool [:{B},{(EqClass (F,B))}:]

{(EqClass (F,B))} is non empty set

[:{B},{(EqClass (F,B))}:] is non empty set

bool [:{B},{(EqClass (F,B))}:] is non empty set

EqClass (F,C) is Element of C

C .--> (EqClass (F,C)) is trivial Relation-like {C} -defined bool (bool Y) -defined {C} -defined C -valued Function-like one-to-one set

{C} is non empty set

{C} --> (EqClass (F,C)) is non empty Relation-like {C} -defined C -valued Function-like constant V17({C}) V21({C},{(EqClass (F,C))}) Element of bool [:{C},{(EqClass (F,C))}:]

{(EqClass (F,C))} is non empty set

[:{C},{(EqClass (F,C))}:] is non empty set

bool [:{C},{(EqClass (F,C))}:] is non empty set

(B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C))) is Relation-like bool (bool Y) -defined Function-like set

EqClass (F,D) is Element of D

D .--> (EqClass (F,D)) is trivial Relation-like {D} -defined bool (bool Y) -defined {D} -defined D -valued Function-like one-to-one set

{D} is non empty set

{D} --> (EqClass (F,D)) is non empty Relation-like {D} -defined D -valued Function-like constant V17({D}) V21({D},{(EqClass (F,D))}) Element of bool [:{D},{(EqClass (F,D))}:]

{(EqClass (F,D))} is non empty set

[:{D},{(EqClass (F,D))}:] is non empty set

bool [:{D},{(EqClass (F,D))}:] is non empty set

((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D))) is Relation-like bool (bool Y) -defined Function-like set

A .--> (EqClass (E,A)) is trivial Relation-like {A} -defined bool (bool Y) -defined {A} -defined A -valued Function-like one-to-one set

{A} is non empty set

{A} --> (EqClass (E,A)) is non empty Relation-like {A} -defined A -valued Function-like constant V17({A}) V21({A},{(EqClass (E,A))}) Element of bool [:{A},{(EqClass (E,A))}:]

{(EqClass (E,A))} is non empty set

[:{A},{(EqClass (E,A))}:] is non empty set

bool [:{A},{(EqClass (E,A))}:] is non empty set

(((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A))) is Relation-like bool (bool Y) -defined Function-like set

((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) . B is set

((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) . D is set

((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) . C is set

rng ((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) is set

((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) . A is set

{(((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) . A),(((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) . B),(((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) . C),(((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) . D)} is non empty set

N is set

dom ((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) is set

z is set

((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) . z is set

N is Element of bool (bool Y)

Intersect N is Element of bool Y

z is set

meet N is Element of bool Y

(EqClass (F,B)) /\ (EqClass (F,C)) is Element of bool Y

((EqClass (F,B)) /\ (EqClass (F,C))) /\ (EqClass (F,D)) is Element of bool Y

(((EqClass (F,B)) /\ (EqClass (F,C))) /\ (EqClass (F,D))) /\ (EqClass (E,A)) is Element of bool Y

EqClass (F,(B '/\' C)) is Element of B '/\' C

(EqClass (F,(B '/\' C))) /\ (EqClass (F,D)) is Element of bool Y

Y is non empty set

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

bool Y is non empty Element of bool (bool Y)

bool Y is non empty set

bool (bool Y) is non empty set

bool (bool Y) is non empty set

bool (bool (bool Y)) is non empty set

bool (PARTITIONS Y) is non empty set

G is Element of bool (PARTITIONS Y)

A is non empty with_non-empty_elements a_partition of Y

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

B is non empty with_non-empty_elements a_partition of Y

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

C is non empty with_non-empty_elements a_partition of Y

D is non empty with_non-empty_elements a_partition of Y

{A,B,C,D} is non empty set

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

E is Element of Y

EqClass (E,(C '/\' D)) is Element of C '/\' D

F is Element of Y

EqClass (F,(C '/\' D)) is Element of C '/\' D

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

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

EqClass (F,B) is Element of B

B .--> (EqClass (F,B)) is trivial Relation-like {B} -defined bool (bool Y) -defined {B} -defined B -valued Function-like one-to-one set

{B} is non empty set

{B} --> (EqClass (F,B)) is non empty Relation-like {B} -defined B -valued Function-like constant V17({B}) V21({B},{(EqClass (F,B))}) Element of bool [:{B},{(EqClass (F,B))}:]

{(EqClass (F,B))} is non empty set

[:{B},{(EqClass (F,B))}:] is non empty set

bool [:{B},{(EqClass (F,B))}:] is non empty set

EqClass (F,C) is Element of C

C .--> (EqClass (F,C)) is trivial Relation-like {C} -defined bool (bool Y) -defined {C} -defined C -valued Function-like one-to-one set

{C} is non empty set

{C} --> (EqClass (F,C)) is non empty Relation-like {C} -defined C -valued Function-like constant V17({C}) V21({C},{(EqClass (F,C))}) Element of bool [:{C},{(EqClass (F,C))}:]

{(EqClass (F,C))} is non empty set

[:{C},{(EqClass (F,C))}:] is non empty set

bool [:{C},{(EqClass (F,C))}:] is non empty set

(B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C))) is Relation-like bool (bool Y) -defined Function-like set

EqClass (F,D) is Element of D

D .--> (EqClass (F,D)) is trivial Relation-like {D} -defined bool (bool Y) -defined {D} -defined D -valued Function-like one-to-one set

{D} is non empty set

{D} --> (EqClass (F,D)) is non empty Relation-like {D} -defined D -valued Function-like constant V17({D}) V21({D},{(EqClass (F,D))}) Element of bool [:{D},{(EqClass (F,D))}:]

{(EqClass (F,D))} is non empty set

[:{D},{(EqClass (F,D))}:] is non empty set

bool [:{D},{(EqClass (F,D))}:] is non empty set

((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D))) is Relation-like bool (bool Y) -defined Function-like set

EqClass (E,A) is Element of A

A .--> (EqClass (E,A)) is trivial Relation-like {A} -defined bool (bool Y) -defined {A} -defined A -valued Function-like one-to-one set

{A} is non empty set

{A} --> (EqClass (E,A)) is non empty Relation-like {A} -defined A -valued Function-like constant V17({A}) V21({A},{(EqClass (E,A))}) Element of bool [:{A},{(EqClass (E,A))}:]

{(EqClass (E,A))} is non empty set

[:{A},{(EqClass (E,A))}:] is non empty set

bool [:{A},{(EqClass (E,A))}:] is non empty set

(((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A))) is Relation-like bool (bool Y) -defined Function-like set

A '/\' (C '/\' D) is non empty with_non-empty_elements a_partition of Y

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

(A '/\' C) '/\' D is non empty with_non-empty_elements a_partition of Y

rng ((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) is set

((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) . A is set

((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) . B is set

((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) . C is set

((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) . D is set

{(((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) . A),(((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) . B),(((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) . C),(((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) . D)} is non empty set

N is set

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

(B '/\' C) '/\' D is non empty with_non-empty_elements a_partition of Y

EqClass (F,((B '/\' C) '/\' D)) is Element of (B '/\' C) '/\' D

EqClass (F,(B '/\' C)) is Element of B '/\' C

(EqClass (F,(B '/\' C))) /\ (EqClass (F,D)) is Element of bool Y

h is set

((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) . h is set

dom ((((B .--> (EqClass (F,B))) +* (C .--> (EqClass (F,C)))) +* (D .--> (EqClass (F,D)))) +* (A .--> (EqClass (E,A)))) is set

N is Element of bool (bool Y)

Intersect N is Element of bool Y

h is set

meet N is Element of bool Y

(EqClass (F,B)) /\ (EqClass (F,C)) is Element of bool Y

((EqClass (F,B)) /\ (EqClass (F,C))) /\ (EqClass (F,D)) is Element of bool Y

(((EqClass (F,B)) /\ (EqClass (