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

Y is Element of R

{Y} is non empty set

R is set

{R} is non empty set

Y is non empty set

{ {b

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

union { (R .: b

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

union { {b

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

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

union { (Class (Y,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

{ {b

union { {b

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

{ H

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

{ H

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

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

union { (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 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

{ H

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

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