:: RELSET_2 semantic presentation

{} 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
{ {b₁} where b₁ 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
{ {b₁} where b₁ 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 .: b₁) where b₁ is Element of bool A : b₁ in B } is set
union { (R .: b₁) where b₁ is Element of bool A : b₁ 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
{ {b₁} where b₁ is Element of A : b₁ in B } is set
union { {b₁} where b₁ is Element of A : b₁ 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
{ {b₁} where b₁ is Element of A : b₁ 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,b₁)) where b₁ is Element of A : b₁ in R } is set
union { (Class (Y,b₁)) where b₁ is Element of A : b₁ 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
{ {b₁} where b₁ is Element of A : b₁ in R } is set
union { {b₁} where b₁ is Element of A : b₁ 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 .: b₁) where b₁ is Element of A : b₁ in R } is set
{ H₁(b₁) where b₁ is Element of A : S₁[b₁] } 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,b₁,Y) where b₁ is Element of bool A : b₁ in R } is set
{ H₁(b₁) where b₁ is Element of bool A : S₁[b₁] } 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,b₁,R) where b₁ is Element of bool A : b₁ 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
{ (b₁ .: R) where b₁ is Relation-like A -defined B -valued Element of bool [:A,B:] : b₁ in Y } is set
union { (b₁ .: R) where b₁ is Relation-like A -defined B -valued Element of bool [:A,B:] : b₁ 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,b₁) where b₁ is Relation-like Y -defined R -valued Element of bool [:Y,R:] : b₁ in R } is set
{ H₁(b₁) where b₁ is Relation-like Y -defined R -valued Element of bool [:Y,R:] : S₁[b₁] } 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,b₁) where b₁ is Relation-like B -defined A -valued Element of bool [:B,A:] : b₁ 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 bool [:A,B:]
R ~ is Relation-like B -defined A -valued Element of bool [:B,A:]
[:B,A:] is Relation-like set
bool [:B,A:] is non empty set
Y is set
R is set
(R ~) .: R is Element of bool A
bool A is non empty set
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
b is set
(B,A,(R ~),b) is Element of bool A
{b} is non empty set
(R ~) .: {b} is set
S is set
a is set
(B,A,(R ~),a) is Element of bool A
{a} is non empty set
(R ~) .: {a} is set
[a,S] is V18() set
{a,S} is non empty set
{{a,S},{a}} is non empty 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
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:]
R ~ is Relation-like B -defined A -valued Element of bool [:B,A:]
[:B,A:] is Relation-like set
bool [:B,A:] is non empty set
Y is set
R is set
R .: Y is Element of bool B
bool B is non empty set
S is set
a is set
(B,A,(R ~),a) is Element of bool A
bool A is non empty set
{a} is non empty set
(R ~) .: {a} 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
[S,a] is V18() set
{S,a} is non empty set
{S} is non empty set
{{S,a},{S}} is non empty set
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
[S,a] is V18() set
{S,a} is non empty set
{S} is non empty set
{{S,a},{S}} is non empty set
(B,A,(R ~),S) is Element of bool A
bool A is non empty set
(R ~) .: {S} is set
A is set
bool A is non empty set
B is set
bool B is non empty 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 B
R is Relation-like A -defined B -valued Element of bool [:A,B:]
R ~ is Relation-like B -defined A -valued Element of bool [:B,A:]
[:B,A:] is Relation-like set
bool [:B,A:] is non empty set
(R ~) .: Y is Element of bool A
R .: R is Element of bool B
S is set
a is set
(B,A,(R ~),a) is Element of bool A
{a} is non empty set
(R ~) .: {a} is set
S is set
a is set
(B,A,(R ~),a) is Element of bool A
{a} is non empty set
(R ~) .: {a} is 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:]
proj1 R is set
Y is set
R .: Y is Element of bool B
bool B is non empty set
Y /\ (proj1 R) is set
R .: (Y /\ (proj1 R)) is Element of bool B
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
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
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:]
R ~ is Relation-like B -defined A -valued Element of bool [:B,A:]
[:B,A:] is Relation-like set
bool [:B,A:] is non empty set
proj2 R is set
Y is set
(R ~) .: Y is Element of bool A
bool A is non empty set
Y /\ (proj2 R) is set
(R ~) .: (Y /\ (proj2 R)) is Element of bool A
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
[R,S] is V18() set
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty 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
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,B,R,Y) ` is Element of bool B
B \ (A,B,R,Y) is set
Y ` is Relation-like A -defined B -valued Element of bool [:A,B:]
[:A,B:] \ Y is Relation-like set
(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,B:] \ Y is Relation-like A -defined B -valued Element of bool [:A,B:]
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,R] is V18() set
{a,R} is non empty set
{a} is non empty set
{{a,R},{a}} is non empty set
(A,B,Y,a) is Element of bool B
Y .: {a} is set
A is set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is set
[:B,R:] is Relation-like set
bool [:B,R:] is non empty set
Y is Relation-like A -defined B -valued Element of bool [:A,B:]
R is Relation-like B -defined R -valued Element of bool [:B,R:]
Y * R is Relation-like A -defined R -valued set
[:A,R:] is Relation-like set
bool [:A,R:] is non empty set
S is Relation-like A -defined B -valued Element of bool [:A,B:]
a is Relation-like B -defined R -valued Element of bool [:B,R:]
S * a is Relation-like A -defined R -valued Element of bool [:A,R:]
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:]
Y .: R is Element of bool B
bool B is non empty set
(Y .: R) ` is Element of bool B
B \ (Y .: R) is set
Y ` is Relation-like A -defined B -valued Element of bool [:A,B:]
[:A,B:] \ Y is Relation-like set
(A,B,R,(Y `)) is Element of bool B
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
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,B,(Y `),S) is Element of bool B
(Y `) .: {S} is set
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
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
B 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:]
proj1 R is set
R ~ is Relation-like A -defined B -valued Element of bool [:A,B:]
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
(R ~) .: A is Element of bool B
bool B is non empty set
proj2 R is set
R .: B is Element of bool A
bool A is non empty set
dom R is Element of bool B
rng (R ~) is Element of bool B
rng R is Element of bool A
A is set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is set
[:B,R:] is Relation-like set
bool [:B,R:] is non empty set
Y is Relation-like A -defined B -valued Element of bool [:A,B:]
Y ~ is Relation-like B -defined A -valued Element of bool [:B,A:]
[:B,A:] is Relation-like set
bool [:B,A:] is non empty set
proj1 Y is set
R is Relation-like B -defined R -valued Element of bool [:B,R:]
(A,B,R,Y,R) is Relation-like A -defined R -valued Element of bool [:A,R:]
[:A,R:] is Relation-like set
bool [:A,R:] is non empty set
proj1 (A,B,R,Y,R) is set
proj1 R is set
(Y ~) .: (proj1 R) is Element of bool A
bool A is non empty set
(A,B,R,Y,R) ~ is Relation-like R -defined A -valued Element of bool [:R,A:]
[:R,A:] is Relation-like set
bool [:R,A:] is non empty set
((A,B,R,Y,R) ~) .: R is Element of bool A
R ~ is Relation-like R -defined B -valued Element of bool [:R,B:]
[:R,B:] is Relation-like set
bool [:R,B:] is non empty set
(R,B,A,(R ~),(Y ~)) is Relation-like R -defined A -valued Element of bool [:R,A:]
(R,B,A,(R ~),(Y ~)) .: R is Element of bool A
(R ~) .: R is Element of bool B
bool B is non empty set
(Y ~) .: ((R ~) .: R) is Element of bool A
dom R is Element of bool B
(Y ~) .: B is Element of bool A
A is set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is set
[:B,R:] is Relation-like set
bool [:B,R:] is non empty set
Y is Relation-like A -defined B -valued Element of bool [:A,B:]
proj2 Y is set
R is Relation-like B -defined R -valued Element of bool [:B,R:]
(A,B,R,Y,R) is Relation-like A -defined R -valued Element of bool [:A,R:]
[:A,R:] is Relation-like set
bool [:A,R:] is non empty set
proj2 (A,B,R,Y,R) is set
R .: (proj2 Y) is Element of bool R
bool R is non empty set
proj2 R is set
(A,B,R,Y,R) .: A is Element of bool R
Y .: A is Element of bool B
bool B is non empty set
R .: (Y .: A) is Element of bool R
rng Y is Element of bool B
R .: B is Element of bool R
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:]
proj1 Y is set
Y ~ is Relation-like B -defined A -valued Element of bool [:B,A:]
[:B,A:] is Relation-like set
bool [:B,A:] is non empty set
(A,B,A,Y,(Y ~)) is Relation-like A -defined A -valued Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
(A,B,A,Y,(Y ~)) .: R is Element of bool A
R is set
S is Element of A
a 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
[a,S] is V18() set
{a,S} is non empty set
{a} is non empty set
{{a,S},{a}} is non empty set
(Y ~) .: {a} is Element of bool A
a is set
[a,a] is V18() set
{a,a} is non empty set
{{a,a},{a}} is non empty 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
[S,a] is V18() set
{S,a} is non empty set
{{S,a},{S}} is non empty set
R is set
Y .: R is Element of bool B
bool B is non empty set
(Y ~) .: (Y .: R) is Element of bool A
(Y ~) .: B is Element of bool A
A is set
B is set
bool B is non empty set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is Element of bool B
Y is Relation-like A -defined B -valued Element of bool [:A,B:]
proj2 Y is set
Y ~ is Relation-like B -defined A -valued Element of bool [:B,A:]
[:B,A:] is Relation-like set
bool [:B,A:] is non empty set
(B,A,B,(Y ~),Y) is Relation-like B -defined B -valued Element of bool [:B,B:]
[:B,B:] is Relation-like set
bool [:B,B:] is non empty set
(B,A,B,(Y ~),Y) .: R is Element of bool B
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
[R,S] is V18() set
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
(A,B,Y,S) is Element of bool B
Y .: {S} is set
Y .: {S} is Element of bool B
a is set
[S,a] is V18() set
{S,a} is non empty set
{{S,a},{S}} is non empty 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
[R,a] is V18() set
{R,a} is non empty set
{{R,a},{R}} is non empty set
R is set
(Y ~) .: R is Element of bool A
bool A is non empty set
Y .: ((Y ~) .: R) is Element of bool B
Y .: A is Element of bool B
B is set
A is set
[:B,A:] is Relation-like set
bool [:B,A:] 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 B -defined A -valued Element of bool [:B,A:]
proj1 R is set
R ~ is Relation-like A -defined B -valued Element of bool [:A,B:]
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
(R ~) .: A is Element of bool B
bool B is non empty set
S is Relation-like R -defined Y -valued Element of bool [:R,Y:]
S ~ is Relation-like Y -defined R -valued Element of bool [:Y,R:]
[:Y,R:] is Relation-like set
bool [:Y,R:] is non empty set
S .: R is Element of bool Y
bool Y is non empty set
(S ~) .: (S .: R) is Element of bool R
bool R is non empty set
proj2 S is set
(S ~) .: (proj2 S) is Element of bool R
A is set
B 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:]
R ~ is Relation-like A -defined B -valued Element of bool [:A,B:]
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
(R ~) .: A is Element of bool B
bool B is non empty set
(B,A,B,R,(R ~)) is Relation-like B -defined B -valued Element of bool [:B,B:]
[:B,B:] is Relation-like set
bool [:B,B:] is non empty set
(B,A,B,R,(R ~)) .: B is Element of bool B
R .: B is Element of bool A
bool A is non empty set
(R ~) .: (R .: B) is Element of bool B
proj2 R is set
(R ~) .: (proj2 R) is Element of bool B
Y is set
A /\ (proj2 R) is set
(R ~) .: (A /\ (proj2 R)) is Element of bool B
((R ~) .: A) /\ ((R ~) .: (proj2 R)) is Element of bool B
Y is set
rng R is Element of bool A
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:]
R .: A is Element of bool B
bool B is non empty set
R ~ is Relation-like B -defined A -valued Element of bool [:B,A:]
[:B,A:] is Relation-like set
bool [:B,A:] is non empty set
(B,A,B,(R ~),R) is Relation-like B -defined B -valued Element of bool [:B,B:]
[:B,B:] is Relation-like set
bool [:B,B:] is non empty set
(B,A,B,(R ~),R) .: B is Element of bool B
(R ~) .: B is Element of bool A
bool A is non empty set
R .: ((R ~) .: B) is Element of bool B
proj1 R is set
R .: (proj1 R) is Element of bool B
Y is set
A /\ (proj1 R) is set
R .: (A /\ (proj1 R)) is Element of bool B
(R .: A) /\ (R .: (proj1 R)) is Element of bool B
Y is set
dom R is Element of bool 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 set
[:B,R:] is Relation-like set
bool [:B,R:] is non empty set
[:A,R:] is Relation-like set
Y is Element of bool A
R is Relation-like A -defined B -valued Element of bool [:A,B:]
R .: Y is Element of bool B
bool B is non empty set
S is Relation-like B -defined R -valued Element of bool [:B,R:]
(B,R,(R .: Y),S) is Element of bool R
bool R is non empty set
bool B is non empty Element of bool (bool B)
bool (bool B) is non empty set
bool R is non empty Element of bool (bool R)
bool (bool R) is non empty set
(R,B,S) is Relation-like bool B -defined bool R -valued Function-like V21( bool B, bool R) Element of bool [:(bool B),(bool R):]
[:(bool B),(bool R):] is non empty Relation-like set
bool [:(bool B),(bool R):] 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
(R,B,S) .: (SmallestPartition (R .: Y)) is Element of bool (bool R)
bool (bool R) is non empty set
Intersect ((R,B,S) .: (SmallestPartition (R .: Y))) is Element of bool R
S ` is Relation-like B -defined R -valued Element of bool [:B,R:]
[:B,R:] \ S is Relation-like set
(A,B,R,R,(S `)) is Relation-like A -defined R -valued Element of bool [:A,R:]
bool [:A,R:] is non empty set
(A,B,R,R,(S `)) ` is Relation-like A -defined R -valued Element of bool [:A,R:]
[:A,R:] \ (A,B,R,R,(S `)) is Relation-like set
(A,R,Y,((A,B,R,R,(S `)) `)) is Element of bool R
bool A is non empty Element of bool (bool A)
bool (bool A) is non empty set
(R,A,((A,B,R,R,(S `)) `)) is Relation-like bool A -defined bool R -valued Function-like V21( bool A, bool R) Element of bool [:(bool A),(bool R):]
[:(bool A),(bool R):] is non empty Relation-like set
bool [:(bool A),(bool R):] 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
(R,A,((A,B,R,R,(S `)) `)) .: (SmallestPartition Y) is Element of bool (bool R)
Intersect ((R,A,((A,B,R,R,(S `)) `)) .: (SmallestPartition Y)) is Element of bool R
(B,R,(R .: Y),S) ` is Element of bool R
R \ (B,R,(R .: Y),S) is set
(S `) .: (R .: Y) is Element of bool R
(A,B,R,R,(S `)) .: Y is Element of bool R
((A,B,R,R,(S `)) .: Y) ` is Element of bool R
R \ ((A,B,R,R,(S `)) .: Y) is set
A is set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
[:B,A:] is Relation-like set
R is Relation-like A -defined B -valued Element of bool [:A,B:]
R ` is Relation-like A -defined B -valued Element of bool [:A,B:]
[:A,B:] \ R is Relation-like set
(R `) ~ is Relation-like B -defined A -valued Element of bool [:B,A:]
bool [:B,A:] is non empty set
R ~ is Relation-like B -defined A -valued Element of bool [:B,A:]
(R ~) ` is Relation-like B -defined A -valued Element of bool [:B,A:]
[:B,A:] \ (R ~) is Relation-like set
[:A,B:] ~ is Relation-like set
([:A,B:] ~) \ (R ~) is Relation-like Element of bool ([:A,B:] ~)
bool ([:A,B:] ~) is non empty set
A is set
bool A is non empty set
B is set
bool B is non empty 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 B
R is Relation-like A -defined B -valued Element of bool [:A,B:]
R ~ is Relation-like B -defined A -valued Element of bool [:B,A:]
[:B,A:] is Relation-like set
bool [:B,A:] is non empty set
(B,A,Y,(R ~)) 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)
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 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
(A,B,(R ~)) .: (SmallestPartition Y) is Element of bool (bool A)
bool (bool A) is non empty set
Intersect ((A,B,(R ~)) .: (SmallestPartition Y)) is Element of bool A
(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):]
[:(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
(B,A,Y,(R ~)) ` is Element of bool A
A \ (B,A,Y,(R ~)) is set
(R ~) ` is Relation-like B -defined A -valued Element of bool [:B,A:]
[:B,A:] \ (R ~) is Relation-like set
((R ~) `) .: Y is Element of bool A
R /\ (((R ~) `) .: Y) is Element of bool A
R ` is Relation-like A -defined B -valued Element of bool [:A,B:]
[:A,B:] \ R is Relation-like set
S is Relation-like A -defined B -valued Element of bool [:A,B:]
S ~ is Relation-like B -defined A -valued Element of bool [:B,A:]
(S ~) .: Y is Element of bool A
S .: R is Element of bool B
R /\ ((S ~) .: Y) is Element of bool A
Y /\ (S .: R) is Element of bool B
(A,B,R,R) ` is Element of bool B
B \ (A,B,R,R) is set
((A,B,R,R) `) /\ Y is Element of bool B
A is set
bool A is non empty set
B is set
bool B is non empty set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
R is Element of bool A
R ` is Element of bool A
A \ R is set
Y is Element of bool B
Y ` is Element of bool B
B \ Y is set
R is Relation-like A -defined B -valued Element of bool [:A,B:]
R .: (R `) is Element of bool B
R ~ is Relation-like B -defined A -valued Element of bool [:B,A:]
[:B,A:] is Relation-like set
bool [:B,A:] is non empty set
(R ~) .: Y is Element of bool 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
S is set
bool S is non empty set
R is set
[:R,S:] is Relation-like set
bool [:R,S:] 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 ~ is Relation-like B -defined A -valued Element of bool [:B,A:]
[:B,A:] is Relation-like set
bool [:B,A:] is non empty set
(B,A,(A,B,R,Y),(Y ~)) is Element of bool A
(A,B,(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 (A,B,R,Y) is a_partition of (A,B,R,Y)
K51((A,B,R,Y)) is Relation-like (A,B,R,Y) -defined (A,B,R,Y) -valued V17((A,B,R,Y)) V24() V26() V27() V31() Element of bool [:(A,B,R,Y),(A,B,R,Y):]
[:(A,B,R,Y),(A,B,R,Y):] is Relation-like set
bool [:(A,B,R,Y),(A,B,R,Y):] is non empty set
Class K51((A,B,R,Y)) is a_partition of (A,B,R,Y)
(A,B,(Y ~)) .: (SmallestPartition (A,B,R,Y)) is Element of bool (bool A)
bool (bool A) is non empty set
Intersect ((A,B,(Y ~)) .: (SmallestPartition (A,B,R,Y))) is Element of bool A
a is Element of bool S
a is Relation-like R -defined S -valued Element of bool [:R,S:]
a ~ is Relation-like S -defined R -valued Element of bool [:S,R:]
[:S,R:] is Relation-like set
bool [:S,R:] is non empty set
(S,R,a,(a ~)) is Element of bool R
bool R is non empty set
bool S is non empty Element of bool (bool S)
bool (bool S) is non empty set
bool R is non empty Element of bool (bool R)
bool (bool R) is non empty set
(R,S,(a ~)) is Relation-like bool S -defined bool R -valued Function-like V21( bool S, bool R) Element of bool [:(bool S),(bool R):]
[:(bool S),(bool R):] is non empty Relation-like set
bool [:(bool S),(bool R):] 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
(R,S,(a ~)) .: (SmallestPartition a) is Element of bool (bool R)
bool (bool R) is non empty set
Intersect ((R,S,(a ~)) .: (SmallestPartition a)) is Element of bool R
(R,S,(S,R,a,(a ~)),a) is Element of bool S
(S,R,a) is Relation-like bool R -defined bool S -valued Function-like V21( bool R, bool S) Element of bool [:(bool R),(bool S):]
[:(bool R),(bool S):] is non empty Relation-like set
bool [:(bool R),(bool S):] is non empty set
SmallestPartition (S,R,a,(a ~)) is a_partition of (S,R,a,(a ~))
K51((S,R,a,(a ~))) is Relation-like (S,R,a,(a ~)) -defined (S,R,a,(a ~)) -valued V17((S,R,a,(a ~))) V24() V26() V27() V31() Element of bool [:(S,R,a,(a ~)),(S,R,a,(a ~)):]
[:(S,R,a,(a ~)),(S,R,a,(a ~)):] is Relation-like set
bool [:(S,R,a,(a ~)),(S,R,a,(a ~)):] is non empty set
Class K51((S,R,a,(a ~))) is a_partition of (S,R,a,(a ~))
(S,R,a) .: (SmallestPartition (S,R,a,(a ~))) is Element of bool (bool S)
bool (bool S) is non empty set
Intersect ((S,R,a) .: (SmallestPartition (S,R,a,(a ~)))) is Element of bool S
A is set
bool A is non empty set
B is set
bool B is non empty 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 B
R is Relation-like A -defined B -valued Element of bool [:A,B:]
(A,B,R,R) is Element of bool B
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
R ~ is Relation-like B -defined A -valued Element of bool [:B,A:]
[:B,A:] is Relation-like set
bool [:B,A:] is non empty set
(B,A,(A,B,R,R),(R ~)) is Element of bool A
(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 (A,B,R,R) is a_partition of (A,B,R,R)
K51((A,B,R,R)) is Relation-like (A,B,R,R) -defined (A,B,R,R) -valued V17((A,B,R,R)) V24() V26() V27() V31() Element of bool [:(A,B,R,R),(A,B,R,R):]
[:(A,B,R,R),(A,B,R,R):] is Relation-like set
bool [:(A,B,R,R),(A,B,R,R):] is non empty set
Class K51((A,B,R,R)) is a_partition of (A,B,R,R)
(A,B,(R ~)) .: (SmallestPartition (A,B,R,R)) is Element of bool (bool A)
bool (bool A) is non empty set
Intersect ((A,B,(R ~)) .: (SmallestPartition (A,B,R,R))) is Element of bool A
(A,B,(B,A,(A,B,R,R),(R ~)),R) is Element of bool B
SmallestPartition (B,A,(A,B,R,R),(R ~)) is a_partition of (B,A,(A,B,R,R),(R ~))
K51((B,A,(A,B,R,R),(R ~))) is Relation-like (B,A,(A,B,R,R),(R ~)) -defined (B,A,(A,B,R,R),(R ~)) -valued V17((B,A,(A,B,R,R),(R ~))) V24() V26() V27() V31() Element of bool [:(B,A,(A,B,R,R),(R ~)),(B,A,(A,B,R,R),(R ~)):]
[:(B,A,(A,B,R,R),(R ~)),(B,A,(A,B,R,R),(R ~)):] is Relation-like set
bool [:(B,A,(A,B,R,R),(R ~)),(B,A,(A,B,R,R),(R ~)):] is non empty set
Class K51((B,A,(A,B,R,R),(R ~))) is a_partition of (B,A,(A,B,R,R),(R ~))
(B,A,R) .: (SmallestPartition (B,A,(A,B,R,R),(R ~))) is Element of bool (bool B)
Intersect ((B,A,R) .: (SmallestPartition (B,A,(A,B,R,R),(R ~)))) is Element of bool B
(B,A,Y,(R ~)) is Element of bool A
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
(A,B,(R ~)) .: (SmallestPartition Y) is Element of bool (bool A)
Intersect ((A,B,(R ~)) .: (SmallestPartition Y)) is Element of bool A
(A,B,(B,A,Y,(R ~)),R) is Element of bool B
SmallestPartition (B,A,Y,(R ~)) is a_partition of (B,A,Y,(R ~))
K51((B,A,Y,(R ~))) is Relation-like (B,A,Y,(R ~)) -defined (B,A,Y,(R ~)) -valued V17((B,A,Y,(R ~))) V24() V26() V27() V31() Element of bool [:(B,A,Y,(R ~)),(B,A,Y,(R ~)):]
[:(B,A,Y,(R ~)),(B,A,Y,(R ~)):] is Relation-like set
bool [:(B,A,Y,(R ~)),(B,A,Y,(R ~)):] is non empty set
Class K51((B,A,Y,(R ~))) is a_partition of (B,A,Y,(R ~))
(B,A,R) .: (SmallestPartition (B,A,Y,(R ~))) is Element of bool (bool B)
Intersect ((B,A,R) .: (SmallestPartition (B,A,Y,(R ~)))) is Element of bool B
(B,A,(A,B,(B,A,Y,(R ~)),R),(R ~)) is Element of bool A
SmallestPartition (A,B,(B,A,Y,(R ~)),R) is a_partition of (A,B,(B,A,Y,(R ~)),R)
K51((A,B,(B,A,Y,(R ~)),R)) is Relation-like (A,B,(B,A,Y,(R ~)),R) -defined (A,B,(B,A,Y,(R ~)),R) -valued V17((A,B,(B,A,Y,(R ~)),R)) V24() V26() V27() V31() Element of bool [:(A,B,(B,A,Y,(R ~)),R),(A,B,(B,A,Y,(R ~)),R):]
[:(A,B,(B,A,Y,(R ~)),R),(A,B,(B,A,Y,(R ~)),R):] is Relation-like set
bool [:(A,B,(B,A,Y,(R ~)),R),(A,B,(B,A,Y,(R ~)),R):] is non empty set
Class K51((A,B,(B,A,Y,(R ~)),R)) is a_partition of (A,B,(B,A,Y,(R ~)),R)
(A,B,(R ~)) .: (SmallestPartition (A,B,(B,A,Y,(R ~)),R)) is Element of bool (bool A)
Intersect ((A,B,(R ~)) .: (SmallestPartition (A,B,(B,A,Y,(R ~)),R))) is Element of bool A
A is set
id A is Relation-like A -defined A -valued V24() V26() V27() V31() set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
id B is Relation-like B -defined B -valued V24() V26() V27() V31() set
R is Relation-like A -defined B -valued Element of bool [:A,B:]
(id A) * R is Relation-like A -defined B -valued set
R * (id B) is Relation-like A -defined B -valued set