{} is empty Relation-like non-empty empty-yielding set
the empty Relation-like non-empty empty-yielding set is empty Relation-like non-empty empty-yielding set
bool {} is non empty set
{{}} is non empty set
A is set
B is set
SmallestPartition B is a_partition of B
K51(B) is Relation-like B -defined B -valued V17(B) V24() V26() V27() V31() Element of bool [:B,B:]
[:B,B:] is Relation-like set
bool [:B,B:] is non empty set
Class K51(B) is a_partition of B
id B is Relation-like B -defined B -valued V24() V26() V27() V31() set
R is set
Im ((id B),R) is set
{R} is non empty set
(id B) .: {R} is set
R is non empty set
{ {b1} where b1 is Element of R : verum } is set
Y is Element of R
{Y} is non empty set
R is set
{R} is non empty set
Y is non empty set
{ {b1} where b1 is Element of Y : verum } is set
A is set
SmallestPartition A is a_partition of A
K51(A) is Relation-like A -defined A -valued V17(A) V24() V26() V27() V31() Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
Class K51(A) is a_partition of A
B is set
R is set
{R} is non empty set
B is set
{B} is non empty set
A is set
SmallestPartition A is a_partition of A
K51(A) is Relation-like A -defined A -valued V17(A) V24() V26() V27() V31() Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
Class K51(A) is a_partition of A
B is set
A \/ B is set
SmallestPartition (A \/ B) is a_partition of A \/ B
K51((A \/ B)) is Relation-like A \/ B -defined A \/ B -valued V17(A \/ B) V24() V26() V27() V31() Element of bool [:(A \/ B),(A \/ B):]
[:(A \/ B),(A \/ B):] is Relation-like set
bool [:(A \/ B),(A \/ B):] is non empty set
Class K51((A \/ B)) is a_partition of A \/ B
SmallestPartition B is a_partition of B
K51(B) is Relation-like B -defined B -valued V17(B) V24() V26() V27() V31() Element of bool [:B,B:]
[:B,B:] is Relation-like set
bool [:B,B:] is non empty set
Class K51(B) is a_partition of B
(SmallestPartition A) \/ (SmallestPartition B) is set
R is set
Y is set
{Y} is non empty set
R is set
Y is set
{Y} is non empty set
Y is set
{Y} is non empty set
A is set
SmallestPartition A is a_partition of A
K51(A) is Relation-like A -defined A -valued V17(A) V24() V26() V27() V31() Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
Class K51(A) is a_partition of A
B is set
A /\ B is set
SmallestPartition (A /\ B) is a_partition of A /\ B
K51((A /\ B)) is Relation-like A /\ B -defined A /\ B -valued V17(A /\ B) V24() V26() V27() V31() Element of bool [:(A /\ B),(A /\ B):]
[:(A /\ B),(A /\ B):] is Relation-like set
bool [:(A /\ B),(A /\ B):] is non empty set
Class K51((A /\ B)) is a_partition of A /\ B
bool B is non empty set
SmallestPartition B is a_partition of B
K51(B) is Relation-like B -defined B -valued V17(B) V24() V26() V27() V31() Element of bool [:B,B:]
[:B,B:] is Relation-like set
bool [:B,B:] is non empty set
Class K51(B) is a_partition of B
(SmallestPartition A) /\ (SmallestPartition B) is Element of bool (bool B)
bool (bool B) is non empty set
R is set
Y is set
{Y} is non empty set
R is set
Y is set
{Y} is non empty set
R is set
{R} is non empty set
A is set
bool A is non empty set
SmallestPartition A is a_partition of A
K51(A) is Relation-like A -defined A -valued V17(A) V24() V26() V27() V31() Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
Class K51(A) is a_partition of A
B is set
A \ B is Element of bool A
SmallestPartition (A \ B) is a_partition of A \ B
K51((A \ B)) is Relation-like A \ B -defined A \ B -valued V17(A \ B) V24() V26() V27() V31() Element of bool [:(A \ B),(A \ B):]
[:(A \ B),(A \ B):] is Relation-like set
bool [:(A \ B),(A \ B):] is non empty set
Class K51((A \ B)) is a_partition of A \ B
SmallestPartition B is a_partition of B
K51(B) is Relation-like B -defined B -valued V17(B) V24() V26() V27() V31() Element of bool [:B,B:]
[:B,B:] is Relation-like set
bool [:B,B:] is non empty set
Class K51(B) is a_partition of B
(SmallestPartition A) \ (SmallestPartition B) is Element of bool (bool A)
bool (bool A) is non empty set
R is set
Y is set
{Y} is non empty set
R is set
{R} is non empty set
R is set
Y is set
{Y} is non empty set
A is set
SmallestPartition A is a_partition of A
K51(A) is Relation-like A -defined A -valued V17(A) V24() V26() V27() V31() Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
Class K51(A) is a_partition of A
B is set
SmallestPartition B is a_partition of B
K51(B) is Relation-like B -defined B -valued V17(B) V24() V26() V27() V31() Element of bool [:B,B:]
[:B,B:] is Relation-like set
bool [:B,B:] is non empty set
Class K51(B) is a_partition of B
R is set
Y is set
{Y} is non empty set
R is set
{R} is non empty set
Y is set
{Y} is non empty set
A is set
bool A is non empty set
bool (bool A) is non empty set
B is Element of bool (bool A)
Intersect B is Element of bool A
R is Element of bool (bool A)
Intersect R is Element of bool A
(Intersect B) /\ (Intersect R) is Element of bool A
B /\ R is Element of bool (bool A)
Intersect (B /\ R) is Element of bool A
B \/ R is Element of bool (bool A)
Intersect (B \/ R) is Element of bool A
A is Relation-like set
B is Relation-like set
A /\ B is Relation-like set
R is Relation-like set
(A /\ B) * R is Relation-like set
A * R is Relation-like set
B * R is Relation-like set
(A * R) /\ (B * R) is Relation-like set
Y is set
R is set
[Y,R] is V18() set
{Y,R} is non empty set
{Y} is non empty set
{{Y,R},{Y}} is non empty set
S is set
[Y,S] is V18() set
{Y,S} is non empty set
{{Y,S},{Y}} is non empty set
[S,R] is V18() set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} is non empty set
A is set
B is set
[B,A] is V18() set
{B,A} is non empty set
{B} is non empty set
{{B,A},{B}} is non empty set
R is Relation-like set
Im (R,B) is set
R .: {B} is set
Y is set
[Y,A] is V18() set
{Y,A} is non empty set
{Y} is non empty set
{{Y,A},{Y}} is non empty set
A is set
B is Relation-like set
Im (B,A) is set
{A} is non empty set
B .: {A} is set
R is Relation-like set
B \/ R is Relation-like set
Im ((B \/ R),A) is set
(B \/ R) .: {A} is set
Im (R,A) is set
R .: {A} is set
(Im (B,A)) \/ (Im (R,A)) is set
Y is set
[A,Y] is V18() set
{A,Y} is non empty set
{{A,Y},{A}} is non empty set
Y is set
[A,Y] is V18() set
{A,Y} is non empty set
{{A,Y},{A}} is non empty set
[A,Y] is V18() set
{A,Y} is non empty set
{{A,Y},{A}} is non empty set
A is set
B is Relation-like set
Im (B,A) is set
{A} is non empty set
B .: {A} is set
R is Relation-like set
B /\ R is Relation-like set
Im ((B /\ R),A) is set
(B /\ R) .: {A} is set
Im (R,A) is set
R .: {A} is set
(Im (B,A)) /\ (Im (R,A)) is set
Y is set
[A,Y] is V18() set
{A,Y} is non empty set
{{A,Y},{A}} is non empty set
Y is set
[A,Y] is V18() set
{A,Y} is non empty set
{{A,Y},{A}} is non empty set
A is set
B is Relation-like set
Im (B,A) is set
{A} is non empty set
B .: {A} is set
R is Relation-like set
B \ R is Relation-like Element of bool B
bool B is non empty set
Im ((B \ R),A) is set
(B \ R) .: {A} is set
Im (R,A) is set
R .: {A} is set
(Im (B,A)) \ (Im (R,A)) is Element of bool (Im (B,A))
bool (Im (B,A)) is non empty set
Y is set
[A,Y] is V18() set
{A,Y} is non empty set
{{A,Y},{A}} is non empty set
Y is set
[A,Y] is V18() set
{A,Y} is non empty set
{{A,Y},{A}} is non empty set
A is set
SmallestPartition A is a_partition of A
K51(A) is Relation-like A -defined A -valued V17(A) V24() V26() V27() V31() Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
Class K51(A) is a_partition of A
B is Relation-like set
B .: (SmallestPartition A) is set
R is Relation-like set
B /\ R is Relation-like set
(B /\ R) .: (SmallestPartition A) is set
R .: (SmallestPartition A) is set
(B .: (SmallestPartition A)) /\ (R .: (SmallestPartition A)) is set
Y is set
R is set
[R,Y] is V18() set
{R,Y} is non empty set
{R} is non empty set
{{R,Y},{R}} is non empty set
A is set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is Relation-like A -defined B -valued Element of bool [:A,B:]
Y is set
Im (R,Y) is set
{Y} is non empty set
R .: {Y} is set
bool B is non empty set
R .: {Y} is Element of bool B
Coim (R,Y) is set
R " {Y} is set
bool A is non empty set
R " {Y} is Element of bool A
A is set
bool A is non empty set
bool (bool A) is non empty set
B is Element of bool (bool A)
union B is Element of bool A
R is Relation-like set
R .: (union B) is set
{ (R .: b1) where b1 is Element of bool A : b1 in B } is set
union { (R .: b1) where b1 is Element of bool A : b1 in B } is set
Y is set
R is set
[R,Y] is V18() set
{R,Y} is non empty set
{R} is non empty set
{{R,Y},{R}} is non empty set
S is set
R .: S is set
Y is set
R is set
S is Element of bool A
R .: S is set
a is set
[a,Y] is V18() set
{a,Y} is non empty set
{a} is non empty set
{{a,Y},{a}} is non empty set
A is non empty set
bool A is non empty set
B is Element of bool A
{ {b1} where b1 is Element of A : b1 in B } is set
union { {b1} where b1 is Element of A : b1 in B } is set
R is set
{R} is non empty set
R is set
Y is set
R is Element of A
{R} is non empty set
A is non empty set
bool A is non empty set
bool (bool A) is non empty set
B is Element of bool A
{ {b1} where b1 is Element of A : b1 in B } is set
bool A is non empty Element of bool (bool A)
R is set
Y is Element of A
{Y} is non empty set
A is non empty set
bool A is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is Element of bool A
Y is Relation-like A -defined B -valued Element of bool [:A,B:]
Y .: R is Element of bool B
bool B is non empty set
{ (Class (Y,b1)) where b1 is Element of A : b1 in R } is set
union { (Class (Y,b1)) where b1 is Element of A : b1 in R } is set
R is set
S is set
[S,R] is V18() set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} is non empty set
{ {b1} where b1 is Element of A : b1 in R } is set
union { {b1} where b1 is Element of A : b1 in R } is set
a is set
a is Element of A
{a} is non empty set
Y .: {a} is Element of bool B
Class (Y,a) is Element of bool B
Y .: {a} is set
R is set
S is set
a is Element of A
Class (Y,a) is Element of bool B
{a} is non empty set
Y .: {a} is set
a is set
b is set
[b,a] is V18() set
{b,a} is non empty set
{b} is non empty set
{{b,a},{b}} is non empty set
A is non empty set
bool A is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
bool B is non empty set
bool (bool B) is non empty set
R is Element of bool A
Y is Relation-like A -defined B -valued Element of bool [:A,B:]
{ (Y .: b1) where b1 is Element of A : b1 in R } is set
{ H1(b1) where b1 is Element of A : S1[b1] } is set
A is set
bool A is non empty Element of bool (bool A)
bool A is non empty set
bool (bool A) is non empty set
B is Relation-like set
R is set
B .: R is set
Y is set
B .: Y is set
R is Relation-like Function-like set
proj1 R is set
Y is set
R . Y is set
B .: Y is set
R is Relation-like Function-like set
proj1 R is set
Y is Relation-like Function-like set
proj1 Y is set
R is set
R . R is set
Y . R is set
B .: R is set
B is set
A is set
[:B,A:] is Relation-like set
bool [:B,A:] is non empty set
A is set
B is set
R is set
[:B,R:] is Relation-like set
bool [:B,R:] is non empty set
Y is Relation-like B -defined R -valued Element of bool [:B,R:]
(B,Y) is Relation-like Function-like set
proj1 (B,Y) is set
(B,Y) . A is set
Y .: A is Element of bool R
bool R is non empty set
bool B is non empty Element of bool (bool B)
bool B is non empty set
bool (bool B) is non empty set
A is set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,R) is Relation-like Function-like set
proj2 (A,R) is set
rng R is Element of bool B
bool B is non empty set
bool (rng R) is non empty Element of bool (bool (rng R))
bool (rng R) is non empty set
bool (bool (rng R)) is non empty set
Y is set
proj1 (A,R) is set
R is set
(A,R) . R is set
R .: R is Element of bool B
A is set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
bool A is non empty Element of bool (bool A)
bool A is non empty set
bool (bool A) is non empty set
R is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,R) is Relation-like Function-like set
rng R is Element of bool B
bool B is non empty set
bool (rng R) is non empty Element of bool (bool (rng R))
bool (rng R) is non empty set
bool (bool (rng R)) is non empty set
[:(bool A),(bool (rng R)):] is non empty Relation-like set
bool [:(bool A),(bool (rng R)):] is non empty set
proj1 (A,R) is set
proj2 (A,R) is set
B is set
A is set
[:B,A:] is Relation-like set
bool [:B,A:] is non empty set
R is Relation-like B -defined A -valued Element of bool [:B,A:]
(B,R) is Relation-like Function-like set
bool B is non empty Element of bool (bool B)
bool B is non empty set
bool (bool B) is non empty set
bool A is non empty Element of bool (bool A)
bool A is non empty set
bool (bool A) is non empty set
[:(bool B),(bool A):] is non empty Relation-like set
bool [:(bool B),(bool A):] is non empty set
proj1 (B,R) is set
rng R is Element of bool A
bool (rng R) is non empty Element of bool (bool (rng R))
bool (rng R) is non empty set
bool (bool (rng R)) is non empty set
[:(bool B),(bool (rng R)):] is non empty Relation-like set
bool [:(bool B),(bool (rng R)):] is non empty set
proj2 (B,R) is set
A is set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
bool A is non empty Element of bool (bool A)
bool A is non empty set
bool (bool A) is non empty set
bool B is non empty Element of bool (bool B)
bool B is non empty set
bool (bool B) is non empty set
union A is set
R is Relation-like A -defined B -valued Element of bool [:A,B:]
(B,A,R) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
[:(bool A),(bool B):] is non empty Relation-like set
bool [:(bool A),(bool B):] is non empty set
(B,A,R) .: A is Element of bool (bool B)
bool (bool B) is non empty set
union ((B,A,R) .: A) is Element of bool B
R .: (union A) is Element of bool B
Y is set
R is set
dom (B,A,R) is Element of bool (bool A)
bool (bool A) is non empty set
S is set
(B,A,R) . S is set
R .: S is Element of bool B
a is set
[a,Y] is V18() set
{a,Y} is non empty set
{a} is non empty set
{{a,Y},{a}} is non empty set
A is set
bool A is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
bool A is non empty Element of bool (bool A)
bool (bool A) is non empty set
bool B is non empty Element of bool (bool B)
bool B is non empty set
bool (bool B) is non empty set
Y is Relation-like A -defined B -valued Element of bool [:A,B:]
(B,A,Y) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
[:(bool A),(bool B):] is non empty Relation-like set
bool [:(bool A),(bool B):] is non empty set
R is Element of bool A
SmallestPartition R is a_partition of R
K51(R) is Relation-like R -defined R -valued V17(R) V24() V26() V27() V31() Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
Class K51(R) is a_partition of R
(B,A,Y) .: (SmallestPartition R) is Element of bool (bool B)
bool (bool B) is non empty set
Intersect ((B,A,Y) .: (SmallestPartition R)) is Element of bool B
A is set
bool A is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is Element of bool A
Y is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,B,R,Y) is set
bool A is non empty Element of bool (bool A)
bool (bool A) is non empty set
bool B is non empty Element of bool (bool B)
bool B is non empty set
bool (bool B) is non empty set
(B,A,Y) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
[:(bool A),(bool B):] is non empty Relation-like set
bool [:(bool A),(bool B):] is non empty set
SmallestPartition R is a_partition of R
K51(R) is Relation-like R -defined R -valued V17(R) V24() V26() V27() V31() Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
Class K51(R) is a_partition of R
(B,A,Y) .: (SmallestPartition R) is Element of bool (bool B)
bool (bool B) is non empty set
Intersect ((B,A,Y) .: (SmallestPartition R)) is Element of bool B
A is set
bool A is non empty set
bool A is non empty Element of bool (bool A)
bool (bool A) is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
bool B is non empty Element of bool (bool B)
bool B is non empty set
bool (bool B) is non empty set
R is Element of bool A
SmallestPartition R is a_partition of R
K51(R) is Relation-like R -defined R -valued V17(R) V24() V26() V27() V31() Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
Class K51(R) is a_partition of R
Y is Relation-like A -defined B -valued Element of bool [:A,B:]
(B,A,Y) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
[:(bool A),(bool B):] is non empty Relation-like set
bool [:(bool A),(bool B):] is non empty set
(B,A,Y) .: (SmallestPartition R) is Element of bool (bool B)
bool (bool B) is non empty set
dom (B,A,Y) is Element of bool (bool A)
bool (bool A) is non empty set
R is set
S is set
{S} is non empty set
a is set
bool R is non empty set
(bool A) /\ (SmallestPartition R) is Element of bool (bool R)
bool (bool R) is non empty set
A is set
bool A is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is set
Y is Element of bool A
R is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,B,Y,R) is Element of bool B
bool B is non empty set
bool A is non empty Element of bool (bool A)
bool (bool A) is non empty set
bool B is non empty Element of bool (bool B)
bool (bool B) is non empty set
(B,A,R) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
[:(bool A),(bool B):] is non empty Relation-like set
bool [:(bool A),(bool B):] is non empty set
SmallestPartition Y is a_partition of Y
K51(Y) is Relation-like Y -defined Y -valued V17(Y) V24() V26() V27() V31() Element of bool [:Y,Y:]
[:Y,Y:] is Relation-like set
bool [:Y,Y:] is non empty set
Class K51(Y) is a_partition of Y
(B,A,R) .: (SmallestPartition Y) is Element of bool (bool B)
bool (bool B) is non empty set
Intersect ((B,A,R) .: (SmallestPartition Y)) is Element of bool B
S is set
(A,B,R,S) is Element of bool B
{S} is non empty set
R .: {S} is set
meet ((B,A,R) .: (SmallestPartition Y)) is Element of bool B
S is set
{S} is non empty set
R .: {S} is Element of bool B
a is set
(B,A,R) . {S} is set
dom (B,A,R) is Element of bool (bool A)
bool (bool A) is non empty set
[{S},(R .: {S})] is V18() set
{{S},(R .: {S})} is non empty set
{{S}} is non empty set
{{{S},(R .: {S})},{{S}}} is non empty set
S is set
(A,B,R,S) is Element of bool B
{S} is non empty set
R .: {S} is set
A is non empty set
B is set
bool B is non empty set
[:B,A:] is Relation-like set
bool [:B,A:] is non empty set
R is Element of bool B
Y is Element of A
R is Relation-like B -defined A -valued Element of bool [:B,A:]
(B,A,R,R) is Element of bool A
bool A is non empty set
bool B is non empty Element of bool (bool B)
bool (bool B) is non empty set
bool A is non empty Element of bool (bool A)
bool (bool A) is non empty set
(A,B,R) is Relation-like bool B -defined bool A -valued Function-like V21( bool B, bool A) Element of bool [:(bool B),(bool A):]
[:(bool B),(bool A):] is non empty Relation-like set
bool [:(bool B),(bool A):] is non empty set
SmallestPartition R is a_partition of R
K51(R) is Relation-like R -defined R -valued V17(R) V24() V26() V27() V31() Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
Class K51(R) is a_partition of R
(A,B,R) .: (SmallestPartition R) is Element of bool (bool A)
bool (bool A) is non empty set
Intersect ((A,B,R) .: (SmallestPartition R)) is Element of bool A
S is set
(B,A,R,S) is Element of bool A
{S} is non empty set
R .: {S} is set
meet ((A,B,R) .: (SmallestPartition R)) is Element of bool A
S is set
a is set
[a,S] is V18() set
{a,S} is non empty set
{a} is non empty set
{{a,S},{a}} is non empty set
a is set
{a} is non empty set
dom (A,B,R) is Element of bool (bool B)
bool (bool B) is non empty set
(A,B,R) . a is set
(B,A,R,a) is Element of bool A
R .: {a} is set
A is set
bool A is non empty set
bool A is non empty Element of bool (bool A)
bool (bool A) is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
bool B is non empty Element of bool (bool B)
bool B is non empty set
bool (bool B) is non empty set
R is Element of bool A
SmallestPartition R is a_partition of R
K51(R) is Relation-like R -defined R -valued V17(R) V24() V26() V27() V31() Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
Class K51(R) is a_partition of R
Y is Element of bool A
R \/ Y is Element of bool A
R is Relation-like A -defined B -valued Element of bool [:A,B:]
(B,A,R) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
[:(bool A),(bool B):] is non empty Relation-like set
bool [:(bool A),(bool B):] is non empty set
(B,A,R) .: (SmallestPartition R) is Element of bool (bool B)
bool (bool B) is non empty set
(A,B,(R \/ Y),R) is Element of bool B
SmallestPartition (R \/ Y) is a_partition of R \/ Y
K51((R \/ Y)) is Relation-like R \/ Y -defined R \/ Y -valued V17(R \/ Y) V24() V26() V27() V31() Element of bool [:(R \/ Y),(R \/ Y):]
[:(R \/ Y),(R \/ Y):] is Relation-like set
bool [:(R \/ Y),(R \/ Y):] is non empty set
Class K51((R \/ Y)) is a_partition of R \/ Y
(B,A,R) .: (SmallestPartition (R \/ Y)) is Element of bool (bool B)
Intersect ((B,A,R) .: (SmallestPartition (R \/ Y))) is Element of bool B
(A,B,Y,R) is Element of bool B
SmallestPartition Y is a_partition of Y
K51(Y) is Relation-like Y -defined Y -valued V17(Y) V24() V26() V27() V31() Element of bool [:Y,Y:]
[:Y,Y:] is Relation-like set
bool [:Y,Y:] is non empty set
Class K51(Y) is a_partition of Y
(B,A,R) .: (SmallestPartition Y) is Element of bool (bool B)
Intersect ((B,A,R) .: (SmallestPartition Y)) is Element of bool B
(SmallestPartition R) \/ (SmallestPartition Y) is set
((B,A,R) .: (SmallestPartition R)) \/ ((B,A,R) .: (SmallestPartition Y)) is Element of bool (bool B)
Intersect (((B,A,R) .: (SmallestPartition R)) \/ ((B,A,R) .: (SmallestPartition Y))) is Element of bool B
A is set
bool A is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is Element of bool A
Y is Element of bool A
R \/ Y is Element of bool A
R is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,B,(R \/ Y),R) is Element of bool B
bool B is non empty set
bool A is non empty Element of bool (bool A)
bool (bool A) is non empty set
bool B is non empty Element of bool (bool B)
bool (bool B) is non empty set
(B,A,R) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
[:(bool A),(bool B):] is non empty Relation-like set
bool [:(bool A),(bool B):] is non empty set
SmallestPartition (R \/ Y) is a_partition of R \/ Y
K51((R \/ Y)) is Relation-like R \/ Y -defined R \/ Y -valued V17(R \/ Y) V24() V26() V27() V31() Element of bool [:(R \/ Y),(R \/ Y):]
[:(R \/ Y),(R \/ Y):] is Relation-like set
bool [:(R \/ Y),(R \/ Y):] is non empty set
Class K51((R \/ Y)) is a_partition of R \/ Y
(B,A,R) .: (SmallestPartition (R \/ Y)) is Element of bool (bool B)
bool (bool B) is non empty set
Intersect ((B,A,R) .: (SmallestPartition (R \/ Y))) is Element of bool B
(A,B,R,R) is Element of bool B
SmallestPartition R is a_partition of R
K51(R) is Relation-like R -defined R -valued V17(R) V24() V26() V27() V31() Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
Class K51(R) is a_partition of R
(B,A,R) .: (SmallestPartition R) is Element of bool (bool B)
Intersect ((B,A,R) .: (SmallestPartition R)) is Element of bool B
(A,B,Y,R) is Element of bool B
SmallestPartition Y is a_partition of Y
K51(Y) is Relation-like Y -defined Y -valued V17(Y) V24() V26() V27() V31() Element of bool [:Y,Y:]
[:Y,Y:] is Relation-like set
bool [:Y,Y:] is non empty set
Class K51(Y) is a_partition of Y
(B,A,R) .: (SmallestPartition Y) is Element of bool (bool B)
Intersect ((B,A,R) .: (SmallestPartition Y)) is Element of bool B
(A,B,R,R) /\ (A,B,Y,R) is Element of bool B
(SmallestPartition R) \/ (SmallestPartition Y) is set
(B,A,R) .: ((SmallestPartition R) \/ (SmallestPartition Y)) is Element of bool (bool B)
Intersect ((B,A,R) .: ((SmallestPartition R) \/ (SmallestPartition Y))) is Element of bool B
((B,A,R) .: (SmallestPartition R)) \/ ((B,A,R) .: (SmallestPartition Y)) is Element of bool (bool B)
Intersect (((B,A,R) .: (SmallestPartition R)) \/ ((B,A,R) .: (SmallestPartition Y))) is Element of bool B
A is non empty set
bool A is non empty set
bool (bool A) is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
bool B is non empty set
bool (bool B) is non empty set
R is Element of bool (bool A)
Y is Relation-like A -defined B -valued Element of bool [:A,B:]
{ (A,B,b1,Y) where b1 is Element of bool A : b1 in R } is set
{ H1(b1) where b1 is Element of bool A : S1[b1] } is set
A is set
bool A is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is Element of bool A
Y is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,B,R,Y) is Element of bool B
bool B is non empty set
bool A is non empty Element of bool (bool A)
bool (bool A) is non empty set
bool B is non empty Element of bool (bool B)
bool (bool B) is non empty set
(B,A,Y) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
[:(bool A),(bool B):] is non empty Relation-like set
bool [:(bool A),(bool B):] is non empty set
SmallestPartition R is a_partition of R
K51(R) is Relation-like R -defined R -valued V17(R) V24() V26() V27() V31() Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
Class K51(R) is a_partition of R
(B,A,Y) .: (SmallestPartition R) is Element of bool (bool B)
bool (bool B) is non empty set
Intersect ((B,A,Y) .: (SmallestPartition R)) is Element of bool B
A is set
bool A is non empty set
bool (bool A) is non empty set
B is non empty set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
bool B is non empty set
bool (bool B) is non empty set
R is Relation-like A -defined B -valued Element of bool [:A,B:]
Y is Element of bool (bool A)
{ (A,B,b1,R) where b1 is Element of bool A : b1 in Y } is set
union Y is Element of bool A
(A,B,(union Y),R) is Element of bool B
bool A is non empty Element of bool (bool A)
bool B is non empty Element of bool (bool B)
(B,A,R) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
[:(bool A),(bool B):] is non empty Relation-like set
bool [:(bool A),(bool B):] is non empty set
SmallestPartition (union Y) is a_partition of union Y
K51((union Y)) is Relation-like union Y -defined union Y -valued V17( union Y) V24() V26() V27() V31() Element of bool [:(union Y),(union Y):]
[:(union Y),(union Y):] is Relation-like set
bool [:(union Y),(union Y):] is non empty set
Class K51((union Y)) is a_partition of union Y
(B,A,R) .: (SmallestPartition (union Y)) is Element of bool (bool B)
bool (bool B) is non empty set
Intersect ((B,A,R) .: (SmallestPartition (union Y))) is Element of bool B
R is Element of bool (bool B)
Intersect R is Element of bool B
{B} is non empty set
S is set
a is Element of bool A
(A,B,a,R) is Element of bool B
SmallestPartition a is a_partition of a
K51(a) is Relation-like a -defined a -valued V17(a) V24() V26() V27() V31() Element of bool [:a,a:]
[:a,a:] is Relation-like set
bool [:a,a:] is non empty set
Class K51(a) is a_partition of a
(B,A,R) .: (SmallestPartition a) is Element of bool (bool B)
Intersect ((B,A,R) .: (SmallestPartition a)) is Element of bool B
meet {B} is set
meet R is Element of bool B
S is set
a is Element of bool A
(A,B,a,R) is Element of bool B
SmallestPartition a is a_partition of a
K51(a) is Relation-like a -defined a -valued V17(a) V24() V26() V27() V31() Element of bool [:a,a:]
[:a,a:] is Relation-like set
bool [:a,a:] is non empty set
Class K51(a) is a_partition of a
(B,A,R) .: (SmallestPartition a) is Element of bool (bool B)
Intersect ((B,A,R) .: (SmallestPartition a)) is Element of bool B
a is set
b is set
x is Element of bool A
(A,B,x,R) is Element of bool B
SmallestPartition x is a_partition of x
K51(x) is Relation-like x -defined x -valued V17(x) V24() V26() V27() V31() Element of bool [:x,x:]
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
Class K51(x) is a_partition of x
(B,A,R) .: (SmallestPartition x) is Element of bool (bool B)
Intersect ((B,A,R) .: (SmallestPartition x)) is Element of bool B
P is Element of B
P is set
(A,B,R,P) is Element of bool B
{P} is non empty set
R .: {P} is set
meet R is Element of bool B
a is set
meet R is Element of bool B
b is Element of B
x is set
(A,B,R,x) is Element of bool B
{x} is non empty set
R .: {x} is set
P is set
P is Element of bool A
(A,B,P,R) is Element of bool B
SmallestPartition P is a_partition of P
K51(P) is Relation-like P -defined P -valued V17(P) V24() V26() V27() V31() Element of bool [:P,P:]
[:P,P:] is Relation-like set
bool [:P,P:] is non empty set
Class K51(P) is a_partition of P
(B,A,R) .: (SmallestPartition P) is Element of bool (bool B)
Intersect ((B,A,R) .: (SmallestPartition P)) is Element of bool B
A is set
bool A is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is Element of bool A
Y is Element of bool A
R is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,B,Y,R) is Element of bool B
bool B is non empty set
bool A is non empty Element of bool (bool A)
bool (bool A) is non empty set
bool B is non empty Element of bool (bool B)
bool (bool B) is non empty set
(B,A,R) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
[:(bool A),(bool B):] is non empty Relation-like set
bool [:(bool A),(bool B):] is non empty set
SmallestPartition Y is a_partition of Y
K51(Y) is Relation-like Y -defined Y -valued V17(Y) V24() V26() V27() V31() Element of bool [:Y,Y:]
[:Y,Y:] is Relation-like set
bool [:Y,Y:] is non empty set
Class K51(Y) is a_partition of Y
(B,A,R) .: (SmallestPartition Y) is Element of bool (bool B)
bool (bool B) is non empty set
Intersect ((B,A,R) .: (SmallestPartition Y)) is Element of bool B
(A,B,R,R) is Element of bool B
SmallestPartition R is a_partition of R
K51(R) is Relation-like R -defined R -valued V17(R) V24() V26() V27() V31() Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
Class K51(R) is a_partition of R
(B,A,R) .: (SmallestPartition R) is Element of bool (bool B)
Intersect ((B,A,R) .: (SmallestPartition R)) is Element of bool B
S is set
a is set
a is set
[a,a] is V18() set
{a,a} is non empty set
{a} is non empty set
{{a,a},{a}} is non empty set
meet ((B,A,R) .: (SmallestPartition R)) is Element of bool B
meet ((B,A,R) .: (SmallestPartition Y)) is Element of bool B
meet ((B,A,R) .: (SmallestPartition R)) is Element of bool B
A is set
bool A is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is Element of bool A
Y is Element of bool A
R /\ Y is Element of bool A
R is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,B,R,R) is Element of bool B
bool B is non empty set
bool A is non empty Element of bool (bool A)
bool (bool A) is non empty set
bool B is non empty Element of bool (bool B)
bool (bool B) is non empty set
(B,A,R) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
[:(bool A),(bool B):] is non empty Relation-like set
bool [:(bool A),(bool B):] is non empty set
SmallestPartition R is a_partition of R
K51(R) is Relation-like R -defined R -valued V17(R) V24() V26() V27() V31() Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
Class K51(R) is a_partition of R
(B,A,R) .: (SmallestPartition R) is Element of bool (bool B)
bool (bool B) is non empty set
Intersect ((B,A,R) .: (SmallestPartition R)) is Element of bool B
(A,B,Y,R) is Element of bool B
SmallestPartition Y is a_partition of Y
K51(Y) is Relation-like Y -defined Y -valued V17(Y) V24() V26() V27() V31() Element of bool [:Y,Y:]
[:Y,Y:] is Relation-like set
bool [:Y,Y:] is non empty set
Class K51(Y) is a_partition of Y
(B,A,R) .: (SmallestPartition Y) is Element of bool (bool B)
Intersect ((B,A,R) .: (SmallestPartition Y)) is Element of bool B
(A,B,R,R) \/ (A,B,Y,R) is Element of bool B
(A,B,(R /\ Y),R) is Element of bool B
SmallestPartition (R /\ Y) is a_partition of R /\ Y
K51((R /\ Y)) is Relation-like R /\ Y -defined R /\ Y -valued V17(R /\ Y) V24() V26() V27() V31() Element of bool [:(R /\ Y),(R /\ Y):]
[:(R /\ Y),(R /\ Y):] is Relation-like set
bool [:(R /\ Y),(R /\ Y):] is non empty set
Class K51((R /\ Y)) is a_partition of R /\ Y
(B,A,R) .: (SmallestPartition (R /\ Y)) is Element of bool (bool B)
Intersect ((B,A,R) .: (SmallestPartition (R /\ Y))) is Element of bool B
S is set
bool Y is non empty set
(SmallestPartition R) /\ (SmallestPartition Y) is Element of bool (bool Y)
bool (bool Y) is non empty set
((B,A,R) .: (SmallestPartition R)) /\ ((B,A,R) .: (SmallestPartition Y)) is Element of bool (bool B)
meet ((B,A,R) .: (SmallestPartition R)) is Element of bool B
a is set
meet (((B,A,R) .: (SmallestPartition R)) /\ ((B,A,R) .: (SmallestPartition Y))) is Element of bool B
Intersect (((B,A,R) .: (SmallestPartition R)) /\ ((B,A,R) .: (SmallestPartition Y))) is Element of bool B
(B,A,R) .: ((SmallestPartition R) /\ (SmallestPartition Y)) is Element of bool (bool B)
Intersect ((B,A,R) .: ((SmallestPartition R) /\ (SmallestPartition Y))) is Element of bool B
meet ((B,A,R) .: (SmallestPartition Y)) is Element of bool B
a is set
meet (((B,A,R) .: (SmallestPartition R)) /\ ((B,A,R) .: (SmallestPartition Y))) is Element of bool B
Intersect (((B,A,R) .: (SmallestPartition R)) /\ ((B,A,R) .: (SmallestPartition Y))) is Element of bool B
(B,A,R) .: ((SmallestPartition R) /\ (SmallestPartition Y)) is Element of bool (bool B)
Intersect ((B,A,R) .: ((SmallestPartition R) /\ (SmallestPartition Y))) is Element of bool B
A is set
bool A is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is Element of bool A
Y is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,B,R,Y) is Element of bool B
bool B is non empty set
bool A is non empty Element of bool (bool A)
bool (bool A) is non empty set
bool B is non empty Element of bool (bool B)
bool (bool B) is non empty set
(B,A,Y) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
[:(bool A),(bool B):] is non empty Relation-like set
bool [:(bool A),(bool B):] is non empty set
SmallestPartition R is a_partition of R
K51(R) is Relation-like R -defined R -valued V17(R) V24() V26() V27() V31() Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
Class K51(R) is a_partition of R
(B,A,Y) .: (SmallestPartition R) is Element of bool (bool B)
bool (bool B) is non empty set
Intersect ((B,A,Y) .: (SmallestPartition R)) is Element of bool B
R is Relation-like A -defined B -valued Element of bool [:A,B:]
Y /\ R is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,B,R,(Y /\ R)) is Element of bool B
(B,A,(Y /\ R)) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
(B,A,(Y /\ R)) .: (SmallestPartition R) is Element of bool (bool B)
Intersect ((B,A,(Y /\ R)) .: (SmallestPartition R)) is Element of bool B
(A,B,R,R) is Element of bool B
(B,A,R) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
(B,A,R) .: (SmallestPartition R) is Element of bool (bool B)
Intersect ((B,A,R) .: (SmallestPartition R)) is Element of bool B
(A,B,R,Y) /\ (A,B,R,R) is Element of bool B
S is set
a is non empty set
a is Element of a
b is set
(A,B,Y,b) is Element of bool B
{b} is non empty set
Y .: {b} is set
(A,B,(Y /\ R),b) is Element of bool B
(Y /\ R) .: {b} is set
(A,B,R,b) is Element of bool B
R .: {b} is set
(A,B,Y,b) /\ (A,B,R,b) is Element of bool B
b is set
(A,B,R,b) is Element of bool B
{b} is non empty set
R .: {b} is set
(A,B,(Y /\ R),b) is Element of bool B
(Y /\ R) .: {b} is set
(A,B,Y,b) is Element of bool B
Y .: {b} is set
(A,B,Y,b) /\ (A,B,R,b) is Element of bool B
S is set
a is non empty set
a is Element of a
b is set
(A,B,(Y /\ R),b) is Element of bool B
{b} is non empty set
(Y /\ R) .: {b} is set
(A,B,Y,b) is Element of bool B
Y .: {b} is set
(A,B,R,b) is Element of bool B
R .: {b} is set
(A,B,Y,b) /\ (A,B,R,b) is Element of bool B
A is set
bool A is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
bool (bool [:A,B:]) is non empty set
R is Element of bool A
Y is Element of bool (bool [:A,B:])
union Y is Relation-like A -defined B -valued Element of bool [:A,B:]
(union Y) .: R is Element of bool B
bool B is non empty set
{ (b1 .: R) where b1 is Relation-like A -defined B -valued Element of bool [:A,B:] : b1 in Y } is set
union { (b1 .: R) where b1 is Relation-like A -defined B -valued Element of bool [:A,B:] : b1 in Y } is set
R is set
S is set
[S,R] is V18() set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} is non empty set
a is set
a is Relation-like A -defined B -valued Element of bool [:A,B:]
a .: R is Element of bool B
b is set
R is set
S is set
a is Relation-like A -defined B -valued Element of bool [:A,B:]
a .: R is Element of bool B
a is set
[a,R] is V18() set
{a,R} is non empty set
{a} is non empty set
{{a,R},{a}} is non empty set
b is set
[b,R] is V18() set
{b,R} is non empty set
{b} is non empty set
{{b,R},{b}} is non empty set
A is set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
bool (bool [:A,B:]) is non empty set
R is Element of bool (bool [:A,B:])
Y is set
bool Y is non empty set
R is set
[:Y,R:] is Relation-like set
bool [:Y,R:] is non empty set
bool R is non empty set
bool (bool R) is non empty set
S is Element of bool Y
{ (Y,R,S,b1) where b1 is Relation-like Y -defined R -valued Element of bool [:Y,R:] : b1 in R } is set
{ H1(b1) where b1 is Relation-like Y -defined R -valued Element of bool [:Y,R:] : S1[b1] } is set
A is set
bool A is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is Element of bool A
Y is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,B,R,Y) is Element of bool B
bool B is non empty set
bool A is non empty Element of bool (bool A)
bool (bool A) is non empty set
bool B is non empty Element of bool (bool B)
bool (bool B) is non empty set
(B,A,Y) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
[:(bool A),(bool B):] is non empty Relation-like set
bool [:(bool A),(bool B):] is non empty set
SmallestPartition R is a_partition of R
K51(R) is Relation-like R -defined R -valued V17(R) V24() V26() V27() V31() Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
Class K51(R) is a_partition of R
(B,A,Y) .: (SmallestPartition R) is Element of bool (bool B)
bool (bool B) is non empty set
Intersect ((B,A,Y) .: (SmallestPartition R)) is Element of bool B
R is set
S is set
(A,B,Y,S) is Element of bool B
{S} is non empty set
Y .: {S} is set
A is set
bool A is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is Element of bool A
Y is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,B,R,Y) is Element of bool B
bool B is non empty set
bool A is non empty Element of bool (bool A)
bool (bool A) is non empty set
bool B is non empty Element of bool (bool B)
bool (bool B) is non empty set
(B,A,Y) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
[:(bool A),(bool B):] is non empty Relation-like set
bool [:(bool A),(bool B):] is non empty set
SmallestPartition R is a_partition of R
K51(R) is Relation-like R -defined R -valued V17(R) V24() V26() V27() V31() Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
Class K51(R) is a_partition of R
(B,A,Y) .: (SmallestPartition R) is Element of bool (bool B)
bool (bool B) is non empty set
Intersect ((B,A,Y) .: (SmallestPartition R)) is Element of bool B
R is set
S is non empty set
a is Element of S
a is set
(A,B,Y,a) is Element of bool B
{a} is non empty set
Y .: {a} is set
[a,a] is V18() set
{a,a} is non empty set
{{a,a},{a}} is non empty set
A is set
bool A is non empty set
bool (bool A) is non empty set
B is set
bool B is non empty set
[:B,A:] is Relation-like set
bool [:B,A:] is non empty set
bool (bool [:B,A:]) is non empty set
R is Element of bool B
Y is Element of bool (bool [:B,A:])
{ (B,A,R,b1) where b1 is Relation-like B -defined A -valued Element of bool [:B,A:] : b1 in Y } is set
Intersect Y is Relation-like B -defined A -valued Element of bool [:B,A:]
(B,A,R,(Intersect Y)) is Element of bool A
bool B is non empty Element of bool (bool B)
bool (bool B) is non empty set
bool A is non empty Element of bool (bool A)
(A,B,(Intersect Y)) is Relation-like bool B -defined bool A -valued Function-like V21( bool B, bool A) Element of bool [:(bool B),(bool A):]
[:(bool B),(bool A):] is non empty Relation-like set
bool [:(bool B),(bool A):] is non empty set
SmallestPartition R is a_partition of R
K51(R) is Relation-like R -defined R -valued V17(R) V24() V26() V27() V31() Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
Class K51(R) is a_partition of R
(A,B,(Intersect Y)) .: (SmallestPartition R) is Element of bool (bool A)
bool (bool A) is non empty set
Intersect ((A,B,(Intersect Y)) .: (SmallestPartition R)) is Element of bool A
R is Element of bool (bool A)
Intersect R is Element of bool A
S is set
{S} is non empty set
meet {S} is set
{A} is non empty set
S is set
a is Relation-like B -defined A -valued Element of bool [:B,A:]
(B,A,R,a) is Element of bool A
(A,B,a) is Relation-like bool B -defined bool A -valued Function-like V21( bool B, bool A) Element of bool [:(bool B),(bool A):]
(A,B,a) .: (SmallestPartition R) is Element of bool (bool A)
Intersect ((A,B,a) .: (SmallestPartition R)) is Element of bool A
{A} is non empty set
S is set
a is Relation-like B -defined A -valued Element of bool [:B,A:]
(B,A,R,a) is Element of bool A
(A,B,a) is Relation-like bool B -defined bool A -valued Function-like V21( bool B, bool A) Element of bool [:(bool B),(bool A):]
(A,B,a) .: (SmallestPartition R) is Element of bool (bool A)
Intersect ((A,B,a) .: (SmallestPartition R)) is Element of bool A
meet {{}} is set
a is set
S is non empty set
a is Element of S
meet R is Element of bool A
b is set
[:B,S:] is Relation-like set
bool [:B,S:] is non empty set
x is Relation-like B -defined S -valued Element of bool [:B,S:]
(B,S,R,x) is Element of bool S
bool S is non empty set
bool S is non empty Element of bool (bool S)
bool (bool S) is non empty set
(S,B,x) is Relation-like bool B -defined bool S -valued Function-like V21( bool B, bool S) Element of bool [:(bool B),(bool S):]
[:(bool B),(bool S):] is non empty Relation-like set
bool [:(bool B),(bool S):] is non empty set
(S,B,x) .: (SmallestPartition R) is Element of bool (bool S)
bool (bool S) is non empty set
Intersect ((S,B,x) .: (SmallestPartition R)) is Element of bool S
P is set
(B,S,x,P) is Element of bool S
{P} is non empty set
x .: {P} is set
(B,A,(Intersect Y),P) is Element of bool A
(Intersect Y) .: {P} is set
[P,a] is V18() set
{P,a} is non empty set
{{P,a},{P}} is non empty set
meet Y is Relation-like B -defined A -valued Element of bool [:B,A:]
a is set
S is non empty set
[:B,S:] is Relation-like set
bool [:B,S:] is non empty set
b is Relation-like B -defined S -valued Element of bool [:B,S:]
(B,S,R,b) is Element of bool S
bool S is non empty set
bool S is non empty Element of bool (bool S)
bool (bool S) is non empty set
(S,B,b) is Relation-like bool B -defined bool S -valued Function-like V21( bool B, bool S) Element of bool [:(bool B),(bool S):]
[:(bool B),(bool S):] is non empty Relation-like set
bool [:(bool B),(bool S):] is non empty set
(S,B,b) .: (SmallestPartition R) is Element of bool (bool S)
bool (bool S) is non empty set
Intersect ((S,B,b) .: (SmallestPartition R)) is Element of bool S
a is Element of S
meet R is Element of bool A
x is set
(B,A,(Intersect Y),x) is Element of bool A
{x} is non empty set
(Intersect Y) .: {x} is set
[x,a] is V18() set
{x,a} is non empty set
{{x,a},{x}} is non empty set
P is set
P is Relation-like B -defined S -valued Element of bool [:B,S:]
(B,S,R,P) is Element of bool S
(S,B,P) is Relation-like bool B -defined bool S -valued Function-like V21( bool B, bool S) Element of bool [:(bool B),(bool S):]
(S,B,P) .: (SmallestPartition R) is Element of bool (bool S)
Intersect ((S,B,P) .: (SmallestPartition R)) is Element of bool S
(B,S,P,x) is Element of bool S
P .: {x} is set
meet Y is Relation-like B -defined A -valued Element of bool [:B,A:]
A is set
bool A is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is Element of bool A
Y is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,B,R,Y) is Element of bool B
bool B is non empty set
bool A is non empty Element of bool (bool A)
bool (bool A) is non empty set
bool B is non empty Element of bool (bool B)
bool (bool B) is non empty set
(B,A,Y) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
[:(bool A),(bool B):] is non empty Relation-like set
bool [:(bool A),(bool B):] is non empty set
SmallestPartition R is a_partition of R
K51(R) is Relation-like R -defined R -valued V17(R) V24() V26() V27() V31() Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
Class K51(R) is a_partition of R
(B,A,Y) .: (SmallestPartition R) is Element of bool (bool B)
bool (bool B) is non empty set
Intersect ((B,A,Y) .: (SmallestPartition R)) is Element of bool B
R is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,B,R,R) is Element of bool B
(B,A,R) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
(B,A,R) .: (SmallestPartition R) is Element of bool (bool B)
Intersect ((B,A,R) .: (SmallestPartition R)) is Element of bool B
S is set
a is non empty set
a is Element of a
b is set
(A,B,R,b) is Element of bool B
{b} is non empty set
R .: {b} is set
(A,B,Y,b) is Element of bool B
Y .: {b} is set
[b,a] is V18() set
{b,a} is non empty set
{{b,a},{b}} is non empty set
A is set
bool A is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is Element of bool A
Y is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,B,R,Y) is Element of bool B
bool B is non empty set
bool A is non empty Element of bool (bool A)
bool (bool A) is non empty set
bool B is non empty Element of bool (bool B)
bool (bool B) is non empty set
(B,A,Y) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
[:(bool A),(bool B):] is non empty Relation-like set
bool [:(bool A),(bool B):] is non empty set
SmallestPartition R is a_partition of R
K51(R) is Relation-like R -defined R -valued V17(R) V24() V26() V27() V31() Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
Class K51(R) is a_partition of R
(B,A,Y) .: (SmallestPartition R) is Element of bool (bool B)
bool (bool B) is non empty set
Intersect ((B,A,Y) .: (SmallestPartition R)) is Element of bool B
R is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,B,R,R) is Element of bool B
(B,A,R) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
(B,A,R) .: (SmallestPartition R) is Element of bool (bool B)
Intersect ((B,A,R) .: (SmallestPartition R)) is Element of bool B
(A,B,R,Y) \/ (A,B,R,R) is Element of bool B
Y \/ R is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,B,R,(Y \/ R)) is Element of bool B
(B,A,(Y \/ R)) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
(B,A,(Y \/ R)) .: (SmallestPartition R) is Element of bool (bool B)
Intersect ((B,A,(Y \/ R)) .: (SmallestPartition R)) is Element of bool B
S is set
a is non empty set
a is Element of a
b is set
(A,B,(Y \/ R),b) is Element of bool B
{b} is non empty set
(Y \/ R) .: {b} is set
(A,B,Y,b) is Element of bool B
Y .: {b} is set
(A,B,R,b) is Element of bool B
R .: {b} is set
(A,B,Y,b) \/ (A,B,R,b) is Element of bool B
a is non empty set
a is Element of a
b is set
(A,B,(Y \/ R),b) is Element of bool B
{b} is non empty set
(Y \/ R) .: {b} is set
(A,B,R,b) is Element of bool B
R .: {b} is set
(A,B,Y,b) is Element of bool B
Y .: {b} is set
(A,B,Y,b) \/ (A,B,R,b) is Element of bool B
A is set
B is set
[B,A] is V18() set
{B,A} is non empty set
{B} is non empty set
{{B,A},{B}} is non empty set
R is set
Y is set
[:R,Y:] is Relation-like set
bool [:R,Y:] is non empty set
R is Relation-like R -defined Y -valued Element of bool [:R,Y:]
R ` is Relation-like R -defined Y -valued Element of bool [:R,Y:]
[:R,Y:] \ R is Relation-like set
(R,Y,(R `),B) is Element of bool Y
bool Y is non empty set
(R `) .: {B} is set
[:R,Y:] \ R is Relation-like R -defined Y -valued Element of bool [:R,Y:]
S is set
[S,A] is V18() set
{S,A} is non empty set
{S} is non empty set
{{S,A},{S}} is non empty set
[:R,Y:] \ R is Relation-like R -defined Y -valued Element of bool [:R,Y:]
A is set
bool A is non empty set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is Element of bool A
Y is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,B,R,Y) is Element of bool B
bool B is non empty set
bool A is non empty Element of bool (bool A)
bool (bool A) is non empty set
bool B is non empty Element of bool (bool B)
bool (bool B) is non empty set
(B,A,Y) is Relation-like bool A -defined bool B -valued Function-like V21( bool A, bool B) Element of bool [:(bool A),(bool B):]
[:(bool A),(bool B):] is non empty Relation-like set
bool [:(bool A),(bool B):] is non empty set
SmallestPartition R is a_partition of R
K51(R) is Relation-like R -defined R -valued V17(R) V24() V26() V27() V31() Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
Class K51(R) is a_partition of R
(B,A,Y) .: (SmallestPartition R) is Element of bool (bool B)
bool (bool B) is non empty set
Intersect ((B,A,Y) .: (SmallestPartition R)) is Element of bool B
Y .: R is Element of bool B
R is set
S is set
(A,B,Y,S) is Element of bool B
{S} is non empty set
Y .: {S} is set
[S,R] is V18() set
{S,R} is non empty set
{{S,R},{S}} is non empty set
A is set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is Relation-like A -defined B -valued Element of