:: MSSUBFAM semantic presentation

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V39() set

the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V39() set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V39() set

I is set

M is Relation-like I -defined Function-like total Function-yielding V25() set

doms M is Relation-like Function-like set

dom (doms M) is set

dom M is set

rngs M is Relation-like Function-like set

dom (rngs M) is set

dom M is set

I is set

M is Relation-like I -defined Function-like total Function-yielding V25() set

doms M is Relation-like I -defined Function-like set

dom (doms M) is set

dom M is set

SF is Relation-like I -defined Function-like set

rngs M is Relation-like I -defined Function-like set

dom (rngs M) is set

dom M is set

SF is Relation-like I -defined Function-like set

F

F

F

I is set

F

F

M is non empty set

SF is set

[:(F

bool [:(F

SF is Relation-like F

[:(F

bool [:(F

i is Relation-like F

B is set

ab is set

F

M is set

SF is set

F

[:(F

bool [:(F

M is Relation-like F

SF is set

i is set

B is set

M . B is set

F

I is Relation-like F

M is set

I . M is set

F

F

[:(F

bool [:(F

SF is Relation-like F

M is Relation-like F

SF is set

F

F

[:(F

bool [:(F

M . SF is Relation-like Function-like set

I is set

bool I is set

bool (bool I) is set

M is Element of bool (bool I)

Intersect M is Element of bool I

union M is Element of bool I

meet M is Element of bool I

I is set

bool I is set

bool (bool I) is set

M is set

SF is Element of bool (bool I)

Intersect SF is Element of bool I

meet SF is Element of bool I

I is set

bool I is set

bool (bool I) is set

M is Element of bool (bool I)

Intersect M is Element of bool I

meet M is Element of bool I

I is set

bool I is set

bool (bool I) is set

M is Element of bool (bool I)

Intersect M is Element of bool I

SF is Element of bool I

meet M is Element of bool I

I is set

bool I is set

bool (bool I) is set

M is set

SF is Element of bool (bool I)

Intersect SF is Element of bool I

meet SF is Element of bool I

I is set

bool I is set

bool (bool I) is set

M is set

SF is set

i is Element of bool (bool I)

Intersect i is Element of bool I

meet i is Element of bool I

I is set

bool I is set

bool (bool I) is set

M is set

SF is set

i is Element of bool (bool I)

Intersect i is Element of bool I

meet i is Element of bool I

I is set

bool I is set

bool (bool I) is set

M is Element of bool (bool I)

Intersect M is Element of bool I

SF is Element of bool (bool I)

Intersect SF is Element of bool I

i is Element of bool (bool I)

SF \/ i is Element of bool (bool I)

Intersect i is Element of bool I

(Intersect SF) /\ (Intersect i) is Element of bool I

meet SF is Element of bool I

(meet SF) /\ I is Element of bool I

(Intersect SF) /\ I is Element of bool I

meet i is Element of bool I

I /\ (meet i) is Element of bool I

I /\ (Intersect i) is Element of bool I

meet i is Element of bool I

meet M is Element of bool I

meet SF is Element of bool I

I is set

bool I is set

bool (bool I) is set

M is Element of bool (bool I)

Intersect M is Element of bool I

SF is Element of bool I

{SF} is non empty finite set

meet M is Element of bool I

I is set

bool I is set

bool (bool I) is set

M is Element of bool (bool I)

Intersect M is Element of bool I

SF is Element of bool I

i is Element of bool I

{SF,i} is non empty finite set

SF /\ i is Element of bool I

meet M is Element of bool I

I is set

M is Relation-like I -defined Function-like total set

SF is Relation-like I -defined Function-like total set

i is set

M . i is set

SF . i is set

I is set

M is Relation-like I -defined Function-like total set

SF is Relation-like non-empty I -defined Function-like total set

i is set

M . i is set

SF . i is set

I is set

M is set

SF is Relation-like M -defined Function-like total Function-yielding V25() set

SF . I is Relation-like Function-like set

rngs SF is Relation-like M -defined Function-like total set

(rngs SF) . I is set

dom SF is set

i is Relation-like Function-like set

rng i is set

I is set

M is set

SF is Relation-like M -defined Function-like total Function-yielding V25() set

SF . I is Relation-like Function-like set

doms SF is Relation-like M -defined Function-like total set

(doms SF) . I is set

dom SF is set

i is Relation-like Function-like set

dom i is set

I is set

M is Relation-like I -defined Function-like total Function-yielding V25() set

SF is Relation-like I -defined Function-like total Function-yielding V25() set

SF ** M is Relation-like Function-like Function-yielding V25() set

dom (SF ** M) is set

dom M is set

dom SF is set

(dom M) /\ (dom SF) is set

I /\ (dom SF) is set

I /\ I is set

I is set

[[0]] I is Relation-like empty-yielding I -defined Function-like total set

I --> {} is Relation-like I -defined {{}} -valued Function-like constant total quasi_total Function-yielding V25() Element of bool [:I,{{}}:]

{{}} is non empty functional finite V39() set

[:I,{{}}:] is Relation-like set

bool [:I,{{}}:] is set

M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total Function-yielding V25() ManySortedFunction of M, [[0]] I

i is set

M . i is set

([[0]] I) . i is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V39() set

[:(M . i),(([[0]] I) . i):] is Relation-like set

bool [:(M . i),(([[0]] I) . i):] is set

SF . i is Relation-like Function-like set

B is empty Relation-like non-empty empty-yielding M . i -defined ([[0]] I) . i -valued Function-like one-to-one constant functional quasi_total Function-yielding V25() finite finite-yielding V39() Element of bool [:(M . i),(([[0]] I) . i):]

I is set

M is Relation-like I -defined Function-like total set

SF is Relation-like I -defined Function-like total set

i is Relation-like I -defined Function-like total Function-yielding V25() set

doms i is Relation-like I -defined Function-like total set

rngs i is Relation-like I -defined Function-like total set

B is set

M . B is set

SF . B is set

[:(M . B),(SF . B):] is Relation-like set

bool [:(M . B),(SF . B):] is set

i . B is Relation-like Function-like set

(doms i) . B is set

ab is Relation-like M . B -defined SF . B -valued Function-like quasi_total Element of bool [:(M . B),(SF . B):]

dom ab is set

B is set

(rngs i) . B is set

SF . B is set

M . B is set

[:(M . B),(SF . B):] is Relation-like set

bool [:(M . B),(SF . B):] is set

i . B is Relation-like Function-like set

ab is Relation-like M . B -defined SF . B -valued Function-like quasi_total Element of bool [:(M . B),(SF . B):]

rng ab is set

I is set

M is Relation-like I -defined Function-like total set

SF is set

M . SF is set

i is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V39() set

I is set

[[0]] I is Relation-like empty-yielding I -defined Function-like total finite-yielding set

I --> {} is Relation-like I -defined {{}} -valued Function-like constant total quasi_total Function-yielding V25() Element of bool [:I,{{}}:]

{{}} is non empty functional finite V39() set

[:I,{{}}:] is Relation-like set

bool [:I,{{}}:] is set

I is set

M is Relation-like I -defined Function-like total set

[[0]] I is Relation-like empty-yielding I -defined Function-like total finite-yielding set

I --> {} is Relation-like I -defined {{}} -valued Function-like constant total quasi_total Function-yielding V25() Element of bool [:I,{{}}:]

[:I,{{}}:] is Relation-like set

bool [:I,{{}}:] is set

i is Relation-like I -defined Function-like total ManySortedSubset of M

I is set

M is Relation-like I -defined Function-like total set

SF is Relation-like I -defined Function-like total set

i is set

M . i is set

SF . i is set

I is set

M is Relation-like I -defined Function-like total finite-yielding set

SF is Relation-like I -defined Function-like total ManySortedSubset of M

i is Relation-like I -defined Function-like total set

I is set

M is Relation-like I -defined Function-like total finite-yielding set

SF is Relation-like I -defined Function-like total finite-yielding set

M \/ SF is Relation-like I -defined Function-like total set

i is set

(M \/ SF) . i is set

M . i is finite set

SF . i is finite set

(M . i) \/ (SF . i) is finite set

I is set

M is Relation-like I -defined Function-like total set

SF is Relation-like I -defined Function-like total finite-yielding set

M /\ SF is Relation-like I -defined Function-like total set

i is set

(M /\ SF) . i is set

M . i is set

SF . i is finite set

(M . i) /\ (SF . i) is finite set

I is set

SF is Relation-like I -defined Function-like total finite-yielding set

M is Relation-like I -defined Function-like total set

SF /\ M is Relation-like I -defined Function-like total finite-yielding set

I is set

SF is Relation-like I -defined Function-like total finite-yielding set

M is Relation-like I -defined Function-like total set

SF \ M is Relation-like I -defined Function-like total set

i is set

(SF \ M) . i is set

SF . i is finite set

M . i is set

(SF . i) \ (M . i) is finite Element of bool (SF . i)

bool (SF . i) is finite V39() set

I is set

SF is Relation-like I -defined Function-like total finite-yielding set

M is Relation-like I -defined Function-like total Function-yielding V25() set

M .:.: SF is Relation-like I -defined Function-like total set

i is set

(M .:.: SF) . i is set

M . i is Relation-like Function-like set

B is Relation-like Function-like set

SF . i is finite set

B .: (SF . i) is finite set

I is set

M is Relation-like I -defined Function-like total finite-yielding set

SF is Relation-like I -defined Function-like total finite-yielding set

[|M,SF|] is Relation-like I -defined Function-like total set

i is set

[|M,SF|] . i is set

M . i is finite set

SF . i is finite set

[:(M . i),(SF . i):] is Relation-like finite set

I is set

M is Relation-like I -defined Function-like total set

SF is Relation-like I -defined Function-like total set

[|SF,M|] is Relation-like I -defined Function-like total set

i is set

SF . i is set

[|SF,M|] . i is set

M . i is set

[:(SF . i),(M . i):] is Relation-like set

I is set

M is Relation-like I -defined Function-like total set

SF is Relation-like I -defined Function-like total set

[|M,SF|] is Relation-like I -defined Function-like total set

i is set

SF . i is set

[|M,SF|] . i is set

M . i is set

[:(M . i),(SF . i):] is Relation-like set

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is set

(bool M) . SF is set

M . SF is set

bool (M . SF) is Element of bool (bool (M . SF))

bool (M . SF) is set

bool (bool (M . SF)) is set

SF is set

M . SF is set

(bool M) . SF is set

bool (M . SF) is Element of bool (bool (M . SF))

bool (M . SF) is set

bool (bool (M . SF)) is set

I is set

M is Relation-like I -defined Function-like total finite-yielding set

bool M is Relation-like non-empty I -defined Function-like total set

I is set

M is Relation-like non-empty I -defined Function-like total set

union M is Relation-like I -defined Function-like total set

SF is set

(union M) . SF is set

M . SF is set

i is Relation-like I -defined Function-like total set

B is set

SF .--> B is Relation-like {SF} -defined Function-like one-to-one finite set

{SF} is non empty finite set

{SF} --> B is non empty Relation-like {SF} -defined {B} -valued Function-like constant total quasi_total finite Element of bool [:{SF},{B}:]

{B} is non empty finite set

[:{SF},{B}:] is Relation-like finite set

bool [:{SF},{B}:] is finite V39() set

i +* (SF .--> B) is Relation-like Function-like set

dom (i +* (SF .--> B)) is set

dom (SF .--> B) is finite set

ab is Relation-like I -defined Function-like total set

ab . SF is set

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

Q is set

ab . Q is set

M . Q is set

i . Q is set

union (M . SF) is set

I is set

M is Relation-like I -defined Function-like total set

union M is Relation-like I -defined Function-like total set

SF is set

M . SF is set

(union M) . SF is set

union (M . SF) is set

SF is Relation-like I -defined Function-like total set

i is set

SF . i is set

(union M) . i is set

M . i is set

union (M . i) is set

I is set

M is Relation-like I -defined Function-like total Function-yielding V25() set

doms M is Relation-like I -defined Function-like total set

rngs M is Relation-like I -defined Function-like total set

SF is set

(rngs M) . SF is set

M . SF is Relation-like Function-like set

(doms M) . SF is set

i is Relation-like Function-like set

dom i is set

rng i is set

I is set

M is Relation-like I -defined Function-like total set

SF is Relation-like I -defined Function-like total Function-yielding V25() set

rngs SF is Relation-like I -defined Function-like total set

i is set

M . i is set

SF . i is Relation-like Function-like set

(rngs SF) . i is set

B is Relation-like Function-like set

rng B is set

B " (M . i) is set

I is set

M is Relation-like I -defined Function-like total finite-yielding set

SF is Relation-like I -defined Function-like total finite-yielding set

(Funcs) (M,SF) is Relation-like I -defined Function-like total set

i is set

((Funcs) (M,SF)) . i is set

M . i is finite set

SF . i is finite set

Funcs ((M . i),(SF . i)) is functional set

I is set

M is Relation-like I -defined Function-like total finite-yielding set

SF is Relation-like I -defined Function-like total finite-yielding set

M \+\ SF is Relation-like I -defined Function-like total set

M \ SF is Relation-like I -defined Function-like total finite-yielding set

SF \ M is Relation-like I -defined Function-like total finite-yielding set

(M \ SF) \/ (SF \ M) is Relation-like I -defined Function-like total finite-yielding set

I is set

M is Relation-like I -defined Function-like total set

SF is Relation-like I -defined Function-like total set

i is Relation-like I -defined Function-like total set

[|SF,i|] is Relation-like I -defined Function-like total set

B is set

SF . B is set

i . B is set

M . B is set

[|SF,i|] . B is set

[:(SF . B),(i . B):] is Relation-like set

B is Relation-like I -defined Function-like total set

ab is set

B . ab is set

SF . ab is set

i . ab is set

M . ab is set

ab is Relation-like I -defined Function-like total set

[|B,ab|] is Relation-like I -defined Function-like total set

Q is set

B . Q is set

Q is set

B . Q is set

SF . Q is set

Q is set

ab . Q is set

Q is set

ab . Q is set

i . Q is set

Q is set

M . Q is set

[|B,ab|] . Q is set

B . Q is set

ab . Q is set

[:(B . Q),(ab . Q):] is Relation-like set

I is set

M is Relation-like I -defined Function-like total set

SF is Relation-like I -defined Function-like total set

i is Relation-like I -defined Function-like total set

[|SF,i|] is Relation-like I -defined Function-like total set

B is set

SF . B is set

M . B is set

i . B is set

[|SF,i|] . B is set

[:(SF . B),(i . B):] is Relation-like set

ab is set

[:ab,(i . B):] is Relation-like set

B is Relation-like I -defined Function-like total set

[|B,i|] is Relation-like I -defined Function-like total set

ab is set

B . ab is set

ab is set

B . ab is set

SF . ab is set

ab is set

M . ab is set

[|B,i|] . ab is set

B . ab is set

i . ab is set

[:(B . ab),(i . ab):] is Relation-like set

I is set

M is Relation-like non-empty I -defined Function-like total finite-yielding set

SF is set

M . SF is finite set

i is Relation-like I -defined Function-like total set

B is Relation-like I -defined Function-like total set

ab is set

Q is set

SF .--> ab is Relation-like {SF} -defined Function-like one-to-one finite set

{SF} is non empty finite set

{SF} --> ab is non empty Relation-like {SF} -defined {ab} -valued Function-like constant total quasi_total finite Element of bool [:{SF},{ab}:]

{ab} is non empty finite set

[:{SF},{ab}:] is Relation-like finite set

bool [:{SF},{ab}:] is finite V39() set

dom (SF .--> ab) is finite set

SF .--> Q is Relation-like {SF} -defined Function-like one-to-one finite set

{SF} --> Q is non empty Relation-like {SF} -defined {Q} -valued Function-like constant total quasi_total finite Element of bool [:{SF},{Q}:]

{Q} is non empty finite set

[:{SF},{Q}:] is Relation-like finite set

bool [:{SF},{Q}:] is finite V39() set

i +* (SF .--> Q) is Relation-like Function-like set

dom (i +* (SF .--> Q)) is set

dom (SF .--> Q) is finite set

K is Relation-like I -defined Function-like total set

K . SF is set

(SF .--> Q) . SF is set

q is set

K . q is set

M . q is finite set

i . q is set

B +* (SF .--> ab) is Relation-like Function-like set

dom (B +* (SF .--> ab)) is set

qb is Relation-like I -defined Function-like total set

qb . SF is set

(SF .--> ab) . SF is set

j is set

qb . j is set

M . j is finite set

B . j is set

i is set

B is set

SF is Relation-like I -defined Function-like total set

i is set

SF . i is set

M . i is finite set

i is Relation-like I -defined Function-like total set

B is set

SF . B is set

i . B is set

M . B is finite set

I is set

M is Relation-like non-empty I -defined Function-like total finite-yielding set

SF is set

M . SF is finite set

i is Relation-like I -defined Function-like total set

B is Relation-like I -defined Function-like total set

ab is set

Q is set

SF .--> ab is Relation-like {SF} -defined Function-like one-to-one finite set

{SF} is non empty finite set

{SF} --> ab is non empty Relation-like {SF} -defined {ab} -valued Function-like constant total quasi_total finite Element of bool [:{SF},{ab}:]

{ab} is non empty finite set

[:{SF},{ab}:] is Relation-like finite set

bool [:{SF},{ab}:] is finite V39() set

dom (SF .--> ab) is finite set

SF .--> Q is Relation-like {SF} -defined Function-like one-to-one finite set

{SF} --> Q is non empty Relation-like {SF} -defined {Q} -valued Function-like constant total quasi_total finite Element of bool [:{SF},{Q}:]

{Q} is non empty finite set

[:{SF},{Q}:] is Relation-like finite set

bool [:{SF},{Q}:] is finite V39() set

i +* (SF .--> Q) is Relation-like Function-like set

dom (i +* (SF .--> Q)) is set

dom (SF .--> Q) is finite set

K is Relation-like I -defined Function-like total set

K . SF is set

(SF .--> Q) . SF is set

q is set

K . q is set

M . q is finite set

i . q is set

B +* (SF .--> ab) is Relation-like Function-like set

dom (B +* (SF .--> ab)) is set

qb is Relation-like I -defined Function-like total set

qb . SF is set

(SF .--> ab) . SF is set

j is set

qb . j is set

M . j is finite set

B . j is set

i is set

B is set

SF is Relation-like I -defined Function-like total set

i is set

SF . i is set

M . i is finite set

i is Relation-like I -defined Function-like total set

B is set

i . B is set

SF . B is set

M . B is finite set

I is set

M is Relation-like I -defined Function-like total Function-yielding V25() set

rngs M is Relation-like I -defined Function-like total set

doms M is Relation-like I -defined Function-like total set

SF is Relation-like I -defined Function-like total set

i is set

M . i is Relation-like Function-like set

(doms M) . i is set

SF . i is set

B is Relation-like Function-like set

rng B is set

(rngs M) . i is set

dom B is set

ab is set

B .: ab is set

i is Relation-like I -defined Function-like total set

M .:.: i is Relation-like I -defined Function-like total set

B is set

i . B is set

(doms M) . B is set

M . B is Relation-like Function-like set

SF . B is set

ab is Relation-like Function-like set

ab .: (i . B) is set

B is set

i . B is set

M . B is Relation-like Function-like set

(doms M) . B is set

SF . B is set

ab is Relation-like Function-like set

ab .: (i . B) is set

B is set

M . B is Relation-like Function-like set

i . B is set

(doms M) . B is set

SF . B is set

(M .:.: i) . B is set

ab is Relation-like Function-like set

ab .: (i . B) is set

I is set

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

[[0]] I is Relation-like empty-yielding I -defined Function-like total finite-yielding set

I --> {} is Relation-like I -defined {{}} -valued Function-like constant total quasi_total Function-yielding V25() Element of bool [:I,{{}}:]

[:I,{{}}:] is Relation-like set

bool [:I,{{}}:] is set

(I,M) is Relation-like non-empty I -defined Function-like total ManySortedSubset of bool M

I is set

[[0]] I is Relation-like empty-yielding I -defined Function-like total finite-yielding set

I --> {} is Relation-like I -defined {{}} -valued Function-like constant total quasi_total Function-yielding V25() Element of bool [:I,{{}}:]

[:I,{{}}:] is Relation-like set

bool [:I,{{}}:] is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

(I,M) is Relation-like non-empty I -defined Function-like total ManySortedSubset of bool M

I is set

M is Relation-like I -defined Function-like total finite-yielding set

bool M is Relation-like non-empty I -defined Function-like total finite-yielding set

(I,M) is Relation-like non-empty I -defined Function-like total finite-yielding ManySortedSubset of bool M

I is non empty set

M is non empty Relation-like I -defined Function-like total set

bool M is non empty Relation-like non-empty non empty-yielding I -defined Function-like total set

SF is non empty Relation-like I -defined Function-like total ManySortedSubset of bool M

i is Element of I

SF . i is set

M . i is set

bool (M . i) is set

bool (bool (M . i)) is set

(I,M) is non empty Relation-like non-empty non empty-yielding I -defined Function-like total ManySortedSubset of bool M

(I,M) . i is non empty set

I is set

M is set

SF is Relation-like M -defined Function-like total set

bool SF is Relation-like non-empty M -defined Function-like total set

SF . I is set

bool (SF . I) is set

bool (bool (SF . I)) is set

i is Relation-like M -defined Function-like total ManySortedSubset of bool SF

i . I is set

(M,SF) is Relation-like non-empty M -defined Function-like total ManySortedSubset of bool SF

(M,SF) . I is set

I is set

M is Relation-like I -defined Function-like total set

SF is Relation-like I -defined Function-like total set

bool SF is Relation-like non-empty I -defined Function-like total set

i is Relation-like I -defined Function-like total ManySortedSubset of bool SF

(I,SF) is Relation-like non-empty I -defined Function-like total ManySortedSubset of bool SF

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

i is Relation-like I -defined Function-like total ManySortedSubset of bool M

SF \/ i is Relation-like I -defined Function-like total set

(I,M) is Relation-like non-empty I -defined Function-like total ManySortedSubset of bool M

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

i is Relation-like I -defined Function-like total ManySortedSubset of bool M

SF /\ i is Relation-like I -defined Function-like total set

(I,M) is Relation-like non-empty I -defined Function-like total ManySortedSubset of bool M

(I,M) /\ (I,M) is Relation-like I -defined Function-like total set

I is set

M is Relation-like I -defined Function-like total set

SF is Relation-like I -defined Function-like total set

bool SF is Relation-like non-empty I -defined Function-like total set

i is Relation-like I -defined Function-like total ManySortedSubset of bool SF

i \ M is Relation-like I -defined Function-like total set

(I,SF) is Relation-like non-empty I -defined Function-like total ManySortedSubset of bool SF

(I,SF) \ M is Relation-like I -defined Function-like total set

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

i is Relation-like I -defined Function-like total ManySortedSubset of bool M

SF \+\ i is Relation-like I -defined Function-like total set

SF \ i is Relation-like I -defined Function-like total set

i \ SF is Relation-like I -defined Function-like total set

(SF \ i) \/ (i \ SF) is Relation-like I -defined Function-like total set

I is set

M is Relation-like I -defined Function-like total set

{M} is Relation-like non-empty I -defined Function-like total finite-yielding set

SF is Relation-like I -defined Function-like total set

bool SF is Relation-like non-empty I -defined Function-like total set

(I,SF) is Relation-like non-empty I -defined Function-like total ManySortedSubset of bool SF

I is set

M is Relation-like I -defined Function-like total set

SF is Relation-like I -defined Function-like total set

bool SF is Relation-like non-empty I -defined Function-like total set

i is Relation-like I -defined Function-like total set

{M,i} is Relation-like non-empty I -defined Function-like total finite-yielding set

{M} is Relation-like non-empty I -defined Function-like total finite-yielding set

{i} is Relation-like non-empty I -defined Function-like total finite-yielding set

{M} \/ {i} is Relation-like I -defined Function-like total finite-yielding set

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

union SF is Relation-like I -defined Function-like total set

i is set

bool i is set

bool (bool i) is set

B is Element of bool (bool i)

union B is Element of bool i

i is set

(union SF) . i is set

M . i is set

SF . i is set

bool (M . i) is set

bool (bool (M . i)) is set

union (SF . i) is set

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

i is set

M . i is set

bool (M . i) is set

bool (bool (M . i)) is set

SF . i is set

B is Element of bool (bool (M . i))

Intersect B is Element of bool (M . i)

I --> (Intersect B) is Relation-like I -defined {(Intersect B)} -valued Function-like constant total quasi_total Element of bool [:I,{(Intersect B)}:]

{(Intersect B)} is non empty finite set

[:I,{(Intersect B)}:] is Relation-like set

bool [:I,{(Intersect B)}:] is set

ab is Relation-like I -defined Function-like total set

ab . i is set

i is Relation-like I -defined Function-like total set

i is Relation-like I -defined Function-like total set

B is Relation-like I -defined Function-like total set

ab is set

M . ab is set

bool (M . ab) is set

bool (bool (M . ab)) is set

SF . ab is set

i . ab is set

B . ab is set

Q is Element of bool (bool (M . ab))

Intersect Q is Element of bool (M . ab)

B9 is Element of bool (bool (M . ab))

Intersect B9 is Element of bool (M . ab)

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

(I,M,SF) is Relation-like I -defined Function-like total set

i is set

(I,M,SF) . i is set

M . i is set

bool (M . i) is set

bool (bool (M . i)) is set

SF . i is set

B is Element of bool (bool (M . i))

Intersect B is Element of bool (M . i)

I is set

[[0]] I is Relation-like empty-yielding I -defined Function-like total finite-yielding set

I --> {} is Relation-like I -defined {{}} -valued Function-like constant total quasi_total Function-yielding V25() Element of bool [:I,{{}}:]

[:I,{{}}:] is Relation-like set

bool [:I,{{}}:] is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

(I,M,SF) is Relation-like I -defined Function-like total ManySortedSubset of M

i is set

M . i is set

bool (M . i) is set

bool (bool (M . i)) is set

SF . i is set

(I,M,SF) . i is set

B is Element of bool (bool (M . i))

Intersect B is Element of bool (M . i)

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like non-empty I -defined Function-like total ManySortedSubset of bool M

(I,M,SF) is Relation-like I -defined Function-like total ManySortedSubset of M

union SF is Relation-like I -defined Function-like total set

i is set

(I,M,SF) . i is set

(union SF) . i is set

M . i is set

bool (M . i) is set

bool (bool (M . i)) is set

SF . i is set

B is Element of bool (bool (M . i))

Intersect B is Element of bool (M . i)

meet B is Element of bool (M . i)

union B is Element of bool (M . i)

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total set

i is Relation-like I -defined Function-like total ManySortedSubset of bool M

(I,M,i) is Relation-like I -defined Function-like total ManySortedSubset of M

B is set

(I,M,i) . B is set

SF . B is set

M . B is set

bool (M . B) is set

bool (bool (M . B)) is set

i . B is set

ab is Element of bool (bool (M . B))

Intersect ab is Element of bool (M . B)

meet ab is Element of bool (M . B)

I is set

[[0]] I is Relation-like empty-yielding I -defined Function-like total finite-yielding set

I --> {} is Relation-like I -defined {{}} -valued Function-like constant total quasi_total Function-yielding V25() Element of bool [:I,{{}}:]

[:I,{{}}:] is Relation-like set

bool [:I,{{}}:] is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

(I,M,SF) is Relation-like I -defined Function-like total ManySortedSubset of M

i is set

M . i is set

bool (M . i) is set

bool (bool (M . i)) is set

SF . i is set

(I,M,SF) . i is set

B is Element of bool (bool (M . i))

Intersect B is Element of bool (M . i)

([[0]] I) . i is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V39() set

meet B is Element of bool (M . i)

I is set

SF is Relation-like I -defined Function-like total set

bool SF is Relation-like non-empty I -defined Function-like total set

M is Relation-like I -defined Function-like total set

i is Relation-like non-empty I -defined Function-like total ManySortedSubset of bool SF

(I,SF,i) is Relation-like I -defined Function-like total ManySortedSubset of SF

B is set

M . B is set

(I,SF,i) . B is set

ab is Relation-like I -defined Function-like total set

SF . B is set

bool (SF . B) is set

bool (bool (SF . B)) is set

i . B is set

Q is Element of bool (bool (SF . B))

Intersect Q is Element of bool (SF . B)

B9 is set

B .--> B9 is Relation-like {B} -defined Function-like one-to-one finite set

{B} is non empty finite set

{B} --> B9 is non empty Relation-like {B} -defined {B9} -valued Function-like constant total quasi_total finite Element of bool [:{B},{B9}:]

{B9} is non empty finite set

[:{B},{B9}:] is Relation-like finite set

bool [:{B},{B9}:] is finite V39() set

ab +* (B .--> B9) is Relation-like Function-like set

dom (ab +* (B .--> B9)) is set

dom (B .--> B9) is finite set

K is Relation-like I -defined Function-like total set

K . B is set

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

q is set

K . q is set

i . q is set

ab . q is set

meet Q is Element of bool (SF . B)

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

(I,M,SF) is Relation-like I -defined Function-like total ManySortedSubset of M

i is Relation-like I -defined Function-like total ManySortedSubset of bool M

(I,M,i) is Relation-like I -defined Function-like total ManySortedSubset of M

B is set

(I,M,i) . B is set

(I,M,SF) . B is set

M . B is set

bool (M . B) is set

bool (bool (M . B)) is set

SF . B is set

ab is Element of bool (bool (M . B))

Intersect ab is Element of bool (M . B)

i . B is set

Q is Element of bool (bool (M . B))

Intersect Q is Element of bool (M . B)

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total set

i is Relation-like I -defined Function-like total set

B is Relation-like I -defined Function-like total ManySortedSubset of bool M

(I,M,B) is Relation-like I -defined Function-like total ManySortedSubset of M

ab is set

(I,M,B) . ab is set

i . ab is set

SF . ab is set

M . ab is set

bool (M . ab) is set

bool (bool (M . ab)) is set

B . ab is set

Q is Element of bool (bool (M . ab))

Intersect Q is Element of bool (M . ab)

meet Q is Element of bool (M . ab)

I is set

[[0]] I is Relation-like empty-yielding I -defined Function-like total finite-yielding set

I --> {} is Relation-like I -defined {{}} -valued Function-like constant total quasi_total Function-yielding V25() Element of bool [:I,{{}}:]

[:I,{{}}:] is Relation-like set

bool [:I,{{}}:] is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total set

i is Relation-like I -defined Function-like total set

SF /\ i is Relation-like I -defined Function-like total set

B is Relation-like I -defined Function-like total ManySortedSubset of bool M

(I,M,B) is Relation-like I -defined Function-like total ManySortedSubset of M

(I,M,B) /\ i is Relation-like I -defined Function-like total set

ab is set

M . ab is set

bool (M . ab) is set

bool (bool (M . ab)) is set

B . ab is set

(I,M,B) . ab is set

Q is Element of bool (bool (M . ab))

Intersect Q is Element of bool (M . ab)

SF . ab is set

i . ab is set

(SF . ab) /\ (i . ab) is set

([[0]] I) . ab is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V39() set

meet Q is Element of bool (M . ab)

(meet Q) /\ (i . ab) is Element of bool (M . ab)

((I,M,B) /\ i) . ab is set

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

(I,M,SF) is Relation-like I -defined Function-like total ManySortedSubset of M

i is Relation-like I -defined Function-like total ManySortedSubset of bool M

(I,M,i) is Relation-like I -defined Function-like total ManySortedSubset of M

B is Relation-like I -defined Function-like total ManySortedSubset of bool M

i \/ B is Relation-like I -defined Function-like total set

(I,M,B) is Relation-like I -defined Function-like total ManySortedSubset of M

(I,M,i) /\ (I,M,B) is Relation-like I -defined Function-like total set

ab is set

M . ab is set

bool (M . ab) is set

bool (bool (M . ab)) is set

i . ab is set

(I,M,i) . ab is set

Q is Element of bool (bool (M . ab))

Intersect Q is Element of bool (M . ab)

SF . ab is set

(I,M,SF) . ab is set

B9 is Element of bool (bool (M . ab))

Intersect B9 is Element of bool (M . ab)

B . ab is set

(I,M,B) . ab is set

K is Element of bool (bool (M . ab))

Intersect K is Element of bool (M . ab)

Q \/ K is Element of bool (bool (M . ab))

meet B9 is Element of bool (M . ab)

meet Q is Element of bool (M . ab)

meet K is Element of bool (M . ab)

(meet Q) /\ (meet K) is Element of bool (M . ab)

((I,M,i) . ab) /\ (meet K) is Element of bool (M . ab)

((I,M,i) . ab) /\ ((I,M,B) . ab) is set

((I,M,i) /\ (I,M,B)) . ab is set

((I,M,i) . ab) /\ (M . ab) is set

((I,M,i) . ab) /\ ((I,M,B) . ab) is set

((I,M,i) /\ (I,M,B)) . ab is set

(M . ab) /\ ((I,M,B) . ab) is set

((I,M,i) . ab) /\ ((I,M,B) . ab) is set

((I,M,i) /\ (I,M,B)) . ab is set

(Intersect Q) /\ (Intersect K) is Element of bool (M . ab)

((I,M,i) /\ (I,M,B)) . ab is set

((I,M,i) /\ (I,M,B)) . ab is set

((I,M,i) /\ (I,M,B)) . ab is set

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

(I,M,SF) is Relation-like I -defined Function-like total ManySortedSubset of M

i is Relation-like I -defined Function-like total ManySortedSubset of M

{i} is Relation-like non-empty I -defined Function-like total finite-yielding set

B is set

M . B is set

bool (M . B) is set

bool (bool (M . B)) is set

SF . B is set

(I,M,SF) . B is set

ab is Element of bool (bool (M . B))

Intersect ab is Element of bool (M . B)

meet ab is Element of bool (M . B)

i . B is set

{(i . B)} is non empty finite set

meet {(i . B)} is set

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

(I,M,SF) is Relation-like I -defined Function-like total ManySortedSubset of M

i is Relation-like I -defined Function-like total ManySortedSubset of M

B is Relation-like I -defined Function-like total ManySortedSubset of M

{i,B} is Relation-like non-empty I -defined Function-like total finite-yielding set

i /\ B is Relation-like I -defined Function-like total set

ab is set

M . ab is set

bool (M . ab) is set

bool (bool (M . ab)) is set

SF . ab is set

(I,M,SF) . ab is set

{i,B} . ab is finite set

meet ({i,B} . ab) is set

i . ab is set

B . ab is set

{(i . ab),(B . ab)} is non empty finite set

meet {(i . ab),(B . ab)} is set

(i . ab) /\ (B . ab) is set

(i /\ B) . ab is set

Q is Element of bool (bool (M . ab))

Intersect Q is Element of bool (M . ab)

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total set

i is Relation-like I -defined Function-like total ManySortedSubset of bool M

(I,M,i) is Relation-like I -defined Function-like total ManySortedSubset of M

B is Relation-like I -defined Function-like total set

ab is set

SF . ab is set

B . ab is set

(I,M,i) . ab is set

i . ab is set

M . ab is set

bool (M . ab) is set

bool (bool (M . ab)) is set

Q is Element of bool (bool (M . ab))

Intersect Q is Element of bool (M . ab)

I is set

SF is Relation-like I -defined Function-like total set

bool SF is Relation-like non-empty I -defined Function-like total set

M is Relation-like I -defined Function-like total set

i is Relation-like non-empty I -defined Function-like total ManySortedSubset of bool SF

(I,SF,i) is Relation-like I -defined Function-like total ManySortedSubset of SF

B is set

M . B is set

(I,SF,i) . B is set

ab is Relation-like I -defined Function-like total set

SF . B is set

bool (SF . B) is set

bool (bool (SF . B)) is set

i . B is set

Q is Element of bool (bool (SF . B))

Intersect Q is Element of bool (SF . B)

B9 is set

B .--> B9 is Relation-like {B} -defined Function-like one-to-one finite set

{B} is non empty finite set

{B} --> B9 is non empty Relation-like {B} -defined {B9} -valued Function-like constant total quasi_total finite Element of bool [:{B},{B9}:]

{B9} is non empty finite set

[:{B},{B9}:] is Relation-like finite set

bool [:{B},{B9}:] is finite V39() set

ab +* (B .--> B9) is Relation-like Function-like set

dom (ab +* (B .--> B9)) is set

dom (B .--> B9) is finite set

K is Relation-like I -defined Function-like total set

K . B is set

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

q is set

K . q is set

i . q is set

ab . q is set

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

I is set

M is Relation-like I -defined Function-like total set

(I,M) is Relation-like non-empty I -defined Function-like total ManySortedSubset of bool M

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total set

i is Relation-like I -defined Function-like total set

SF \/ i is Relation-like I -defined Function-like total set

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

union SF is Relation-like I -defined Function-like total set

SF is Relation-like I -defined Function-like total set

i is Relation-like I -defined Function-like total set

SF /\ i is Relation-like I -defined Function-like total set

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

(I,M,SF) is Relation-like I -defined Function-like total ManySortedSubset of M

[[0]] I is Relation-like empty-yielding I -defined Function-like total finite-yielding set

I --> {} is Relation-like I -defined {{}} -valued Function-like constant total quasi_total Function-yielding V25() Element of bool [:I,{{}}:]

[:I,{{}}:] is Relation-like set

bool [:I,{{}}:] is set

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

(I,M) is Relation-like non-empty I -defined Function-like total ManySortedSubset of bool M

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

i is Relation-like I -defined Function-like total set

B is Relation-like I -defined Function-like total set

i \/ B is Relation-like I -defined Function-like total set

{i} is Relation-like non-empty I -defined Function-like total finite-yielding set

{B} is Relation-like non-empty I -defined Function-like total finite-yielding set

{i} \/ {B} is Relation-like I -defined Function-like total finite-yielding set

{i,B} is Relation-like non-empty I -defined Function-like total finite-yielding set

union {i,B} is Relation-like I -defined Function-like total set

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

i is Relation-like I -defined Function-like total set

B is Relation-like I -defined Function-like total set

i /\ B is Relation-like I -defined Function-like total set

{i,B} is Relation-like non-empty I -defined Function-like total finite-yielding set

{i} is Relation-like non-empty I -defined Function-like total finite-yielding set

{B} is Relation-like non-empty I -defined Function-like total finite-yielding set

{i} \/ {B} is Relation-like I -defined Function-like total finite-yielding set

ab is Relation-like I -defined Function-like total ManySortedSubset of bool M

(I,M,ab) is Relation-like I -defined Function-like total ManySortedSubset of M

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

[[0]] I is Relation-like empty-yielding I -defined Function-like total finite-yielding set

I --> {} is Relation-like I -defined {{}} -valued Function-like constant total quasi_total Function-yielding V25() Element of bool [:I,{{}}:]

[:I,{{}}:] is Relation-like set

bool [:I,{{}}:] is set

(I,M) is Relation-like non-empty I -defined Function-like total (I,M) (I,M) (I,M) (I,M) (I,M) (I,M) ManySortedSubset of bool M

i is Relation-like I -defined Function-like total ManySortedSubset of bool M

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

(I,M,SF) is Relation-like I -defined Function-like total ManySortedSubset of M

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

i is set

SF . i is set

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

[[0]] I is Relation-like empty-yielding I -defined Function-like total finite-yielding set

I --> {} is Relation-like I -defined {{}} -valued Function-like constant total quasi_total Function-yielding V25() Element of bool [:I,{{}}:]

[:I,{{}}:] is Relation-like set

bool [:I,{{}}:] is set

(I,M) is Relation-like non-empty I -defined Function-like total (I,M) (I,M) (I,M) (I,M) (I,M) (I,M) ManySortedSubset of bool M

i is Relation-like I -defined Function-like total ManySortedSubset of bool M

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

union SF is Relation-like I -defined Function-like total set

I is set

M is Relation-like I -defined Function-like total set

bool M is Relation-like non-empty I -defined Function-like total set

SF is Relation-like I -defined Function-like total ManySortedSubset of bool M

[[0]] I is Relation-like empty-yielding I -defined Function-like total finite-yielding set

I --> {} is Relation-like I -defined {{}} -valued Function-like constant total quasi_total Function-yielding V25() Element of bool [:I,{{}}:]

[:I,{{}}:] is Relation-like set

bool [:I,{{}}:] is set

i is set

SF . i is set