:: 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₁() is set
F₂() is Relation-like F₁() -defined Function-like total set
F₃() is Relation-like F₁() -defined Function-like total set
I is set
F₃() . I is set
F₂() . I is set
M is non empty set
SF is set
[:(F₂() . I),M:] is Relation-like set
bool [:(F₂() . I),M:] is set
SF is Relation-like F₂() . I -defined M -valued Function-like total quasi_total Element of bool [:(F₂() . I),M:]
[:(F₂() . I),(F₃() . I):] is Relation-like set
bool [:(F₂() . I),(F₃() . I):] is set
i is Relation-like F₂() . I -defined F₃() . I -valued Function-like quasi_total Element of bool [:(F₂() . I),(F₃() . I):]
B is set
ab is set
F₃() . I is set
M is set
SF is set
F₂() . I is set
[:(F₂() . I),(F₃() . I):] is Relation-like set
bool [:(F₂() . I),(F₃() . I):] is set
M is Relation-like F₂() . I -defined F₃() . I -valued Function-like quasi_total Element of bool [:(F₂() . I),(F₃() . I):]
SF is set
i is set
B is set
M . B is set
F₃() . I is set
I is Relation-like F₁() -defined Function-like total set
M is set
I . M is set
F₂() . M is set
F₃() . M is set
[:(F₂() . M),(F₃() . M):] is Relation-like set
bool [:(F₂() . M),(F₃() . M):] is set
SF is Relation-like F₂() . M -defined F₃() . M -valued Function-like quasi_total Element of bool [:(F₂() . M),(F₃() . M):]
M is Relation-like F₁() -defined Function-like total Function-yielding V25() ManySortedFunction of F₂(),F₃()
SF is set
F₂() . SF is set
F₃() . SF is set
[:(F₂() . SF),(F₃() . SF):] is Relation-like set
bool [:(F₂() . SF),(F₃() . SF):] is set
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