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