:: CLOSURE2 semantic presentation

K149() is Element of bool K145()
K145() is set
bool K145() is non empty set
K137() is set
bool K137() is non empty set
bool K149() is non empty set
1 is non empty set
{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V45() set
the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V45() set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V45() set
S is set
S is set
S is non empty set
id S is non empty Relation-like S -defined S -valued Function-like one-to-one V17(S) quasi_total Element of bool [:S,S:]
[:S,S:] is non empty Relation-like set
bool [:S,S:] is non empty set
D is Element of S
M is Element of S
(id S) . D is Element of S
(id S) . M is Element of S
S is non empty set
D is non empty Relation-like S -defined Function-like V17(S) set
bool D is non empty Relation-like S -defined Function-like V17(S) additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of bool D
bool D is non empty Relation-like S -defined Function-like V17(S) set
rng (bool D) is non empty set
union (rng (bool D)) is set
M is non empty Relation-like S -defined Function-like V17(S) ManySortedSubset of D
rng M is non empty set
F is set
d is set
M . d is set
dom (bool D) is non empty set
D . d is set
bool (D . d) is non empty Element of bool (bool (D . d))
bool (D . d) is non empty set
bool (bool (D . d)) is non empty set
(bool D) . d is set
S is set
D is Relation-like S -defined Function-like V17(S) set
bool D is Relation-like S -defined Function-like V17(S) additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of bool D
bool D is Relation-like S -defined Function-like V17(S) set
rng (bool D) is set
union (rng (bool D)) is set
Funcs (S,(union (rng (bool D)))) is functional set
M is set
F is set
d is Relation-like S -defined Function-like V17(S) ManySortedSubset of D
dom d is set
rng d is set
[[0]] {} is empty Relation-like non-empty empty-yielding {} -defined Function-like one-to-one constant functional V17( {} ) Function-yielding V25() finite finite-yielding V45() set
{} --> {} is empty Relation-like non-empty empty-yielding {} -defined Function-like one-to-one constant functional V17( {} ) quasi_total Function-yielding V25() finite finite-yielding V45() Element of bool [:{},{{}}:]
{{}} is non empty functional finite V45() set
[:{},{{}}:] is Relation-like finite set
bool [:{},{{}}:] is non empty finite V45() set
{([[0]] {})} is non empty functional finite V45() set
M is set
F is empty Relation-like non-empty empty-yielding {} -defined Function-like one-to-one constant functional V17( {} ) Function-yielding V25() finite finite-yielding V45() set
d is empty Relation-like non-empty empty-yielding {} -defined Function-like one-to-one constant functional V17( {} ) Function-yielding V25() finite finite-yielding V45() ManySortedSubset of F
F is Relation-like S -defined Function-like V17(S) ManySortedSubset of D
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is set
M is set
M is Relation-like Function-like set
F is Relation-like Function-like set
dom M is set
dom F is set
S is set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
(S,D) is non empty functional with_common_domain Element of bool (S,D)
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is functional Element of bool (S,D)
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is non empty functional Element of bool (S,D)
F is Relation-like Function-like Element of M
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is functional Element of bool (S,D)
F is functional Element of bool (S,D)
M \/ F is functional Element of bool (S,D)
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is functional Element of bool (S,D)
F is functional Element of bool (S,D)
M /\ F is functional Element of bool (S,D)
S is set
M is Relation-like S -defined Function-like V17(S) set
(S,M) is non empty functional with_common_domain set
bool (S,M) is non empty set
F is functional Element of bool (S,M)
D is set
F \ D is functional Element of bool (S,M)
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is functional Element of bool (S,D)
F is functional Element of bool (S,D)
M \+\ F is functional Element of bool (S,D)
M \ F is set
F \ M is set
(M \ F) \/ (F \ M) is set
S is set
D is Relation-like S -defined Function-like V17(S) set
{D} is non empty functional finite set
M is Relation-like S -defined Function-like V17(S) set
(S,M) is non empty functional with_common_domain set
bool (S,M) is non empty set
(S,M) is non empty functional with_common_domain Element of bool (S,M)
S is set
D is Relation-like S -defined Function-like V17(S) set
M is Relation-like S -defined Function-like V17(S) set
(S,M) is non empty functional with_common_domain set
bool (S,M) is non empty set
F is Relation-like S -defined Function-like V17(S) set
{D,F} is non empty functional finite set
{D} is non empty functional finite set
{F} is non empty functional finite set
{D} \/ {F} is non empty finite set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
M /\ F is Relation-like S -defined Function-like V17(S) set
D /\ D is Relation-like S -defined Function-like V17(S) set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
M \/ F is Relation-like S -defined Function-like V17(S) set
D \/ D is Relation-like S -defined Function-like V17(S) set
S is set
D is Relation-like S -defined Function-like V17(S) set
M is Relation-like S -defined Function-like V17(S) set
(S,M) is non empty functional with_common_domain Element of bool (S,M)
(S,M) is non empty functional with_common_domain set
bool (S,M) is non empty set
F is Relation-like S -defined Function-like V17(S) (S,M,(S,M))
F \ D is Relation-like S -defined Function-like V17(S) set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
M \+\ F is Relation-like S -defined Function-like V17(S) set
M \ F is Relation-like S -defined Function-like V17(S) set
F \ M is Relation-like S -defined Function-like V17(S) set
(M \ F) \/ (F \ M) is Relation-like S -defined Function-like V17(S) set
S is functional set
D is non empty functional set
{ (b₁ . a₁) where b₁ is Relation-like Function-like Element of D : verum } is set
{ (dom b₁) where b₁ is Relation-like Function-like Element of D : verum } is set
meet { (dom b₁) where b₁ is Relation-like Function-like Element of D : verum } is set
M is Relation-like Function-like set
dom M is set
F is set
M . F is set
{ (b₁ . F) where b₁ is Relation-like Function-like Element of D : verum } is set
D is Relation-like Function-like set
dom D is set
M is Relation-like Function-like set
dom M is set
F is non empty functional set
{ (dom b₁) where b₁ is Relation-like Function-like Element of F : verum } is set
meet { (dom b₁) where b₁ is Relation-like Function-like Element of F : verum } is set
F is non empty functional set
{ (dom b₁) where b₁ is Relation-like Function-like Element of F : verum } is set
meet { (dom b₁) where b₁ is Relation-like Function-like Element of F : verum } is set
d is set
D . d is set
{ (b₁ . d) where b₁ is Relation-like Function-like Element of F : verum } is set
M . d is set
f is non empty functional set
{ (dom b₁) where b₁ is Relation-like Function-like Element of f : verum } is set
meet { (dom b₁) where b₁ is Relation-like Function-like Element of f : verum } is set
d is non empty functional set
{ (dom b₁) where b₁ is Relation-like Function-like Element of d : verum } is set
meet { (dom b₁) where b₁ is Relation-like Function-like Element of d : verum } is set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is non empty functional Element of bool (S,D)
(M) is Relation-like Function-like set
dom (M) is set
F is non empty functional set
{ (dom b₁) where b₁ is Relation-like Function-like Element of F : verum } is set
meet { (dom b₁) where b₁ is Relation-like Function-like Element of F : verum } is set
{S} is non empty finite set
d is set
f is Relation-like Function-like Element of F
dom f is set
the Relation-like Function-like Element of F is Relation-like Function-like Element of F
f is set
dom the Relation-like Function-like Element of F is set
S is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V45() set
(S) is Relation-like Function-like set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is functional Element of bool (S,D)
(M) is Relation-like Function-like set
[[0]] S is Relation-like empty-yielding S -defined Function-like V17(S) set
S --> {} is Relation-like S -defined Function-like constant V17(S) quasi_total Function-yielding V25() Element of bool [:S,{{}}:]
{{}} is non empty functional finite V45() set
[:S,{{}}:] is Relation-like set
bool [:S,{{}}:] is non empty set
dom (M) is set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V45() Element of bool (S,D)
(S,D,M) is Relation-like S -defined Function-like V17(S) set
[[0]] S is Relation-like empty-yielding S -defined Function-like V17(S) set
S --> {} is Relation-like S -defined Function-like constant V17(S) quasi_total Function-yielding V25() Element of bool [:S,{{}}:]
[:S,{{}}:] is Relation-like set
bool [:S,{{}}:] is non empty set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
(S,D) is non empty functional with_common_domain Element of bool (S,D)
M is functional Element of bool (S,D)
(S,D,M) is Relation-like S -defined Function-like V17(S) set
dom (S,D,M) is set
(M) is Relation-like Function-like set
dom (M) is set
F is non empty functional set
{ (dom b₁) where b₁ is Relation-like Function-like Element of F : verum } is set
meet { (dom b₁) where b₁ is Relation-like Function-like Element of F : verum } is set
d is set
(S,D,M) . d is set
{ (b₁ . d) where b₁ is Relation-like S -defined Function-like V17(S) (S,D,(S,D)) : b₁ in M } is set
{ (b₁ . d) where b₁ is Relation-like Function-like Element of F : verum } is set
x is set
SF is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
SF . d is set
x is set
SF is Relation-like Function-like Element of F
SF . d is set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is non empty functional Element of bool (S,D)
(S,D,M) is Relation-like S -defined Function-like V17(S) set
F is set
(S,D,M) . F is set
(S,D) is non empty functional with_common_domain Element of bool (S,D)
{ (b₁ . F) where b₁ is Relation-like S -defined Function-like V17(S) (S,D,(S,D)) : b₁ in M } is set
d is set
f is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
f . F is set
S is Relation-like Function-like set
{S} is non empty functional finite set
({S}) is Relation-like Function-like set
dom ({S}) is set
dom S is set
D is non empty functional set
{ (dom b₁) where b₁ is Relation-like Function-like Element of D : verum } is set
meet { (dom b₁) where b₁ is Relation-like Function-like Element of D : verum } is set
{(dom S)} is non empty finite set
F is set
d is Relation-like Function-like Element of D
dom d is set
F is set
S is Relation-like Function-like set
dom S is set
D is Relation-like Function-like set
{S,D} is non empty functional finite set
({S,D}) is Relation-like Function-like set
dom ({S,D}) is set
dom D is set
(dom S) /\ (dom D) is set
M is non empty functional set
{ (dom b₁) where b₁ is Relation-like Function-like Element of M : verum } is set
meet { (dom b₁) where b₁ is Relation-like Function-like Element of M : verum } is set
{(dom S),(dom D)} is non empty finite set
d is set
f is Relation-like Function-like Element of M
dom f is set
d is set
S is set
D is Relation-like Function-like set
dom D is set
{D} is non empty functional finite set
({D}) is Relation-like Function-like set
({D}) . S is set
D . S is set
{(D . S)} is non empty finite set
dom ({D}) is set
M is non empty functional set
{ (dom b₁) where b₁ is Relation-like Function-like Element of M : verum } is set
meet { (dom b₁) where b₁ is Relation-like Function-like Element of M : verum } is set
{ (b₁ . S) where b₁ is Relation-like Function-like Element of M : verum } is set
F is set
d is Relation-like Function-like Element of M
d . S is set
F is set
S is set
D is set
M is Relation-like D -defined Function-like V17(D) set
(D,M) is non empty functional with_common_domain set
bool (D,M) is non empty set
F is Relation-like Function-like set
{F} is non empty functional finite set
F . S is set
{(F . S)} is non empty finite set
d is functional Element of bool (D,M)
(D,M,d) is Relation-like D -defined Function-like V17(D) set
(D,M,d) . S is set
(d) is Relation-like Function-like set
dom (D,M,d) is set
dom F is set
S is set
D is Relation-like Function-like set
D . S is set
M is Relation-like Function-like set
{D,M} is non empty functional finite set
({D,M}) is Relation-like Function-like set
dom ({D,M}) is set
({D,M}) . S is set
M . S is set
{(D . S),(M . S)} is non empty finite set
F is non empty functional set
{ (dom b₁) where b₁ is Relation-like Function-like Element of F : verum } is set
meet { (dom b₁) where b₁ is Relation-like Function-like Element of F : verum } is set
{ (b₁ . S) where b₁ is Relation-like Function-like Element of F : verum } is set
d is set
f is Relation-like Function-like Element of F
f . S is set
d is set
S is set
D is set
M is Relation-like D -defined Function-like V17(D) set
(D,M) is non empty functional with_common_domain set
bool (D,M) is non empty set
F is Relation-like Function-like set
F . S is set
d is Relation-like Function-like set
{F,d} is non empty functional finite set
d . S is set
{(F . S),(d . S)} is non empty finite set
f is functional Element of bool (D,M)
(D,M,f) is Relation-like D -defined Function-like V17(D) set
(D,M,f) . S is set
dom (D,M,f) is set
(f) is Relation-like Function-like set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is functional Element of bool (S,D)
(S,D,M) is Relation-like S -defined Function-like V17(S) set
bool D is Relation-like S -defined Function-like V17(S) set
bool D is Relation-like S -defined Function-like V17(S) additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of bool D
F is set
(S,D,M) . F is set
(bool D) . F is set
(S,D) is non empty functional with_common_domain Element of bool (S,D)
{ (b₁ . F) where b₁ is Relation-like S -defined Function-like V17(S) (S,D,(S,D)) : b₁ in M } is set
d is set
f is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
f . F is set
D . F is set
bool (D . F) is non empty Element of bool (bool (D . F))
bool (D . F) is non empty set
bool (bool (D . F)) is non empty set
[[0]] S is Relation-like empty-yielding S -defined Function-like V17(S) set
S --> {} is Relation-like S -defined Function-like constant V17(S) quasi_total Function-yielding V25() Element of bool [:S,{{}}:]
[:S,{{}}:] is Relation-like set
bool [:S,{{}}:] is non empty set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is Relation-like S -defined Function-like V17(S) set
F is functional Element of bool (S,D)
(S,D,F) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D
bool D is Relation-like S -defined Function-like V17(S) set
d is set
M . d is set
(S,D,F) . d is set
(S,D) is non empty functional with_common_domain Element of bool (S,D)
{ (b₁ . d) where b₁ is Relation-like S -defined Function-like V17(S) (S,D,(S,D)) : b₁ in F } is set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is Relation-like S -defined Function-like V17(S) set
F is Relation-like S -defined Function-like V17(S) set
{M,F} is non empty functional finite set
M \/ F is Relation-like S -defined Function-like V17(S) set
d is functional Element of bool (S,D)
(S,D,d) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D
bool D is Relation-like S -defined Function-like V17(S) set
union (S,D,d) is Relation-like S -defined Function-like V17(S) set
f is set
(union (S,D,d)) . f is set
(S,D,d) . f is set
union ((S,D,d) . f) is set
M . f is set
F . f is set
{(M . f),(F . f)} is non empty finite set
union {(M . f),(F . f)} is set
(M . f) \/ (F . f) is set
(M \/ F) . f is set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
(S,D) is non empty functional with_common_domain Element of bool (S,D)
M is functional Element of bool (S,D)
(S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D
bool D is Relation-like S -defined Function-like V17(S) set
meet (S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of D
F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
{F,d} is non empty functional finite set
F /\ d is Relation-like S -defined Function-like V17(S) set
q is set
D . q is set
bool (D . q) is non empty set
bool (bool (D . q)) is non empty set
f is non empty functional Element of bool (S,D)
(S,D,f) is Relation-like non-empty S -defined Function-like V17(S) ManySortedSubset of bool D
(S,D,f) . q is set
meet (S,D,f) is Relation-like S -defined Function-like V17(S) ManySortedSubset of D
(meet (S,D,f)) . q is set
(meet (S,D,M)) . q is set
meet ((S,D,f) . q) is set
F . q is set
d . q is set
{(F . q),(d . q)} is non empty finite set
meet {(F . q),(d . q)} is set
(F . q) /\ (d . q) is set
(F /\ d) . q is set
x is Element of bool (bool (D . q))
Intersect x is Element of bool (D . q)
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is functional Element of bool (S,D)
(S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D
bool D is Relation-like S -defined Function-like V17(S) set
meet (S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of D
F is Relation-like S -defined Function-like V17(S) ManySortedSubset of D
d is set
F . d is set
(meet (S,D,M)) . d is set
D . d is set
bool (D . d) is non empty set
bool (bool (D . d)) is non empty set
(S,D,M) . d is set
f is Element of bool (bool (D . d))
Intersect f is Element of bool (D . d)
q is set
(S,D) is non empty functional with_common_domain Element of bool (S,D)
{ (b₁ . d) where b₁ is Relation-like S -defined Function-like V17(S) (S,D,(S,D)) : b₁ in M } is set
x is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
x . d is set
[[0]] S is Relation-like empty-yielding S -defined Function-like V17(S) set
S --> {} is Relation-like S -defined Function-like constant V17(S) quasi_total Function-yielding V25() Element of bool [:S,{{}}:]
[:S,{{}}:] is Relation-like set
bool [:S,{{}}:] is non empty set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
(S,D,(S,D)) is Relation-like non-empty S -defined Function-like V17(S) ManySortedSubset of bool D
bool D is Relation-like S -defined Function-like V17(S) set
bool D is Relation-like S -defined Function-like V17(S) additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of bool D
M is set
(S,D,(S,D)) . M is set
{ (b₁ . M) where b₁ is Relation-like S -defined Function-like V17(S) (S,D,(S,D)) : b₁ in (S,D) } is set
(bool D) . M is set
F is set
d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
d . M is set
D . M is set
bool (D . M) is non empty Element of bool (bool (D . M))
bool (D . M) is non empty set
bool (bool (D . M)) is non empty set
F is set
[[0]] S is Relation-like empty-yielding S -defined Function-like V17(S) set
S --> {} is Relation-like S -defined Function-like constant V17(S) quasi_total Function-yielding V25() Element of bool [:S,{{}}:]
[:S,{{}}:] is Relation-like set
bool [:S,{{}}:] is non empty set
M .--> F is Relation-like {M} -defined Function-like one-to-one finite set
{M} is non empty finite set
{M} --> F is non empty Relation-like {M} -defined Function-like constant V17({M}) quasi_total finite Element of bool [:{M},{F}:]
{F} is non empty finite set
[:{M},{F}:] is non empty Relation-like finite set
bool [:{M},{F}:] is non empty finite V45() set
([[0]] S) +* (M .--> F) is Relation-like Function-like set
dom (([[0]] S) +* (M .--> F)) is set
dom (M .--> F) is finite set
d is Relation-like S -defined Function-like V17(S) set
d . M is set
(M .--> F) . M is set
f is set
d . f is set
D . f is set
bool (D . f) is non empty Element of bool (bool (D . f))
bool (D . f) is non empty set
bool (bool (D . f)) is non empty set
([[0]] S) . f is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V45() set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is Relation-like S -defined Function-like V17(S) set
F is Relation-like S -defined Function-like V17(S) set
M \/ F is Relation-like S -defined Function-like V17(S) set
M is functional Element of bool (S,D)
(S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D
bool D is Relation-like S -defined Function-like V17(S) set
union (S,D,M) is Relation-like S -defined Function-like V17(S) set
M is Relation-like S -defined Function-like V17(S) set
F is Relation-like S -defined Function-like V17(S) set
M /\ F is Relation-like S -defined Function-like V17(S) set
M is functional Element of bool (S,D)
(S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D
bool D is Relation-like S -defined Function-like V17(S) set
meet (S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of D
[[0]] S is Relation-like empty-yielding S -defined Function-like V17(S) set
S --> {} is Relation-like S -defined Function-like constant V17(S) quasi_total Function-yielding V25() Element of bool [:S,{{}}:]
[:S,{{}}:] is Relation-like set
bool [:S,{{}}:] is non empty set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
(S,D) is non empty functional with_common_domain Element of bool (S,D)
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is functional Element of bool (S,D)
F is Relation-like S -defined Function-like V17(S) set
d is Relation-like S -defined Function-like V17(S) set
F \/ d is Relation-like S -defined Function-like V17(S) set
{F,d} is non empty functional finite set
{F} is non empty functional finite set
{d} is non empty functional finite set
{F} \/ {d} is non empty finite set
f is functional Element of bool (S,D)
(S,D,f) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D
bool D is Relation-like S -defined Function-like V17(S) set
union (S,D,f) is Relation-like S -defined Function-like V17(S) set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is functional Element of bool (S,D)
F is Relation-like S -defined Function-like V17(S) set
d is Relation-like S -defined Function-like V17(S) set
F /\ d is Relation-like S -defined Function-like V17(S) set
{F,d} is non empty functional finite set
{F} is non empty functional finite set
{d} is non empty functional finite set
{F} \/ {d} is non empty finite set
f is functional Element of bool (S,D)
(S,D,f) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D
bool D is Relation-like S -defined Function-like V17(S) set
meet (S,D,f) is Relation-like S -defined Function-like V17(S) ManySortedSubset of D
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
F is functional Element of bool (S,D)
M is functional Element of bool (S,D)
(S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D
bool D is Relation-like S -defined Function-like V17(S) set
[[0]] S is Relation-like empty-yielding S -defined Function-like V17(S) set
S --> {} is Relation-like S -defined Function-like constant V17(S) quasi_total Function-yielding V25() Element of bool [:S,{{}}:]
[:S,{{}}:] is Relation-like set
bool [:S,{{}}:] is non empty set
meet (S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of D
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is functional Element of bool (S,D)
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
F is functional Element of bool (S,D)
M is functional Element of bool (S,D)
(S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D
bool D is Relation-like S -defined Function-like V17(S) set
[[0]] S is Relation-like empty-yielding S -defined Function-like V17(S) set
S --> {} is Relation-like S -defined Function-like constant V17(S) quasi_total Function-yielding V25() Element of bool [:S,{{}}:]
[:S,{{}}:] is Relation-like set
bool [:S,{{}}:] is non empty set
union (S,D,M) is Relation-like S -defined Function-like V17(S) set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
M is functional Element of bool (S,D)
S is set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
[:(S,D),(S,D):] is non empty Relation-like set
bool [:(S,D),(S,D):] is non empty set
M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
M . F is set
M . F is Relation-like Function-like Element of (S,D)
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
[:(S,D),(S,D):] is non empty Relation-like set
bool [:(S,D),(S,D):] is non empty set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
[:(S,D),(S,D):] is non empty Relation-like set
bool [:(S,D),(S,D):] is non empty set
id (S,D) is non empty Relation-like (S,D) -defined (S,D) -valued Function-like one-to-one V17((S,D)) quasi_total Function-yielding V25() Element of bool [:(S,D),(S,D):]
M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,(S,D,M,F)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
F \/ d is Relation-like S -defined Function-like V17(S) set
M . (F \/ d) is set
(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,F) \/ (S,D,M,d) is Relation-like S -defined Function-like V17(S) set
(S,D,M,F) \/ d is Relation-like S -defined Function-like V17(S) set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
id (S,D) is non empty Relation-like (S,D) -defined (S,D) -valued Function-like one-to-one V17((S,D)) quasi_total Function-yielding V25() Element of bool [:(S,D),(S,D):]
[:(S,D),(S,D):] is non empty Relation-like set
bool [:(S,D),(S,D):] is non empty set
M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
id (S,D) is non empty Relation-like (S,D) -defined (S,D) -valued Function-like one-to-one V17((S,D)) quasi_total Function-yielding V25() Element of bool [:(S,D),(S,D):]
[:(S,D),(S,D):] is non empty Relation-like set
bool [:(S,D),(S,D):] is non empty set
M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
id (S,D) is non empty Relation-like (S,D) -defined (S,D) -valued Function-like one-to-one V17((S,D)) quasi_total Function-yielding V25() Element of bool [:(S,D),(S,D):]
[:(S,D),(S,D):] is non empty Relation-like set
bool [:(S,D),(S,D):] is non empty set
M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,(S,D,M,F)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
id (S,D) is non empty Relation-like (S,D) -defined (S,D) -valued Function-like one-to-one V17((S,D)) quasi_total Function-yielding V25() Element of bool [:(S,D),(S,D):]
[:(S,D),(S,D):] is non empty Relation-like set
bool [:(S,D),(S,D):] is non empty set
M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
F \/ d is Relation-like S -defined Function-like V17(S) set
M . (F \/ d) is set
(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,F) \/ (S,D,M,d) is Relation-like S -defined Function-like V17(S) set
(S,D,M,F) \/ d is Relation-like S -defined Function-like V17(S) set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)
[:(S,D),(S,D):] is non empty Relation-like set
bool [:(S,D),(S,D):] is non empty set
M is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
F is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
(S,D,F,M) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
[:(S,D),(S,D):] is non empty Relation-like set
bool [:(S,D),(S,D):] is non empty set
M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,(S,D,M,F)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)
[:(S,D),(S,D):] is non empty Relation-like set
bool [:(S,D),(S,D):] is non empty set
M is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
M /\ F is Relation-like S -defined Function-like V17(S) set
d is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
(S,D,d,M) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,d,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,d,M) /\ (S,D,d,F) is Relation-like S -defined Function-like V17(S) set
f is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,d,f) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
[:(S,D),(S,D):] is non empty Relation-like set
bool [:(S,D),(S,D):] is non empty set
M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,F) \/ (S,D,M,d) is Relation-like S -defined Function-like V17(S) set
F \/ d is Relation-like S -defined Function-like V17(S) set
M . (F \/ d) is set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)
[:(S,D),(S,D):] is non empty Relation-like set
bool [:(S,D),(S,D):] is non empty set
M is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
M \ F is Relation-like S -defined Function-like V17(S) set
d is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
(S,D,d,M) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,d,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,d,M) \ (S,D,d,F) is Relation-like S -defined Function-like V17(S) set
f is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,d,f) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,d,M) \/ (S,D,d,F) is Relation-like S -defined Function-like V17(S) set
M \/ F is Relation-like S -defined Function-like V17(S) set
d . (M \/ F) is set
(M \ F) \/ F is Relation-like S -defined Function-like V17(S) set
d . ((M \ F) \/ F) is set
(S,D,d,f) \/ (S,D,d,F) is Relation-like S -defined Function-like V17(S) set
((S,D,d,f) \/ (S,D,d,F)) \ (S,D,d,F) is Relation-like S -defined Function-like V17(S) set
(S,D,d,f) \ (S,D,d,F) is Relation-like S -defined Function-like V17(S) set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
[:(S,D),(S,D):] is non empty Relation-like set
bool [:(S,D),(S,D):] is non empty set
M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
F is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
M * F is Relation-like Function-like set
F * M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
[:(S,D),(S,D):] is non empty Relation-like set
bool [:(S,D),(S,D):] is non empty set
M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
F is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
(S,D,F,M) is non empty Relation-like Function-like V17((S,D)) quasi_total quasi_total Element of bool [:(S,D),(S,D):]
d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,(S,D,F,M),d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,F,d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,(S,D,F,d)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
dom F is non empty set
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
[:(S,D),(S,D):] is non empty Relation-like set
bool [:(S,D),(S,D):] is non empty set
M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
F is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
(S,D,F,M) is non empty Relation-like Function-like V17((S,D)) quasi_total quasi_total Element of bool [:(S,D),(S,D):]
dom F is non empty set
d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
f is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,(S,D,F,M),d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,(S,D,F,M),f) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,F,d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,F,f) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,(S,D,F,d)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,(S,D,F,f)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
[:(S,D),(S,D):] is non empty Relation-like set
bool [:(S,D),(S,D):] is non empty set
M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
F is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
(S,D,F,M) is non empty Relation-like Function-like V17((S,D)) quasi_total quasi_total Element of bool [:(S,D),(S,D):]
(S,D,M,F) is non empty Relation-like Function-like V17((S,D)) quasi_total quasi_total Element of bool [:(S,D),(S,D):]
d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,(S,D,F,M),d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,(S,D,F,M),(S,D,(S,D,F,M),d)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
dom M is non empty set
dom F is non empty set
(S,D,F,d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,(S,D,F,d)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,F,(S,D,F,d)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,(S,D,F,(S,D,F,d))) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,(S,D,M,(S,D,F,(S,D,F,d)))) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,(S,D,M,F),(S,D,F,d)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,(S,D,(S,D,M,F),(S,D,F,d))) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,F,(S,D,M,(S,D,F,d))) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,(S,D,F,(S,D,M,(S,D,F,d)))) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,F,(S,D,(S,D,F,M),d)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,(S,D,F,(S,D,(S,D,F,M),d))) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
S is set
D is Relation-like S -defined Function-like V17(S) set
(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)
(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
[:(S,D),(S,D):] is non empty Relation-like set
bool [:(S,D),(S,D):] is non empty set
M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
F is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]
(S,D,F,M) is non empty Relation-like Function-like V17((S,D)) quasi_total quasi_total Element of bool [:(S,D),(S,D):]
d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
f is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
d \/ f is Relation-like S -defined Function-like V17(S) set
(S,D,F,M) . (d \/ f) is set
(S,D,(S,D,F,M),d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,(S,D,F,M),f) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,(S,D,F,M),d) \/ (S,D,(S,D,F,M),f) is Relation-like S -defined Function-like V17(S) set
dom F is non empty set
F . (d \/ f) is set
M . (F . (d \/ f)) is set
(S,D,F,d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,F,f) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,F,d) \/ (S,D,F,f) is Relation-like S -defined Function-like V17(S) set
M . ((S,D,F,d) \/ (S,D,F,f)) is set
(S,D,M,(S,D,F,d)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,(S,D,F,f)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
(S,D,M,(S,D,F,d)) \/ (S,D,M,(S,D,F,f)) is Relation-like S -defined Function-like V17(S) set
(S,D,(S,D,F,M),d) \/ (S,D,M,(S,D,F,f)) is Relation-like S -defined Function-like V17(S) set
S is 1-sorted
S is 1-sorted
D is many-sorted over S
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the carrier of S is set
( the carrier of S, the Sorts of D) is non empty functional with_common_domain ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
(S, the Sorts of D,( the carrier of S, the Sorts of D)) is (S) (S)
S is 1-sorted
D is many-sorted over S
(S,D) is (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the carrier of S is set
( the carrier of S, the Sorts of D) is non empty functional with_common_domain ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
(S, the Sorts of D,( the carrier of S, the Sorts of D)) is (S) (S)
the Sorts of (S,D) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the of (S,D) is functional Element of bool ( the carrier of S, the Sorts of (S,D))
( the carrier of S, the Sorts of (S,D)) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of (S,D)) is non empty set
S is 1-sorted
D is non-empty many-sorted over S
(S,D) is (S) (S) (S) (S) (S) (S) (S) (S)
the Sorts of D is Relation-like non-empty the carrier of S -defined Function-like V17( the carrier of S) set
the carrier of S is set
( the carrier of S, the Sorts of D) is non empty functional with_common_domain ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
(S, the Sorts of D,( the carrier of S, the Sorts of D)) is (S) (S)
S is 1-sorted
the non-empty many-sorted over S is non-empty many-sorted over S
(S, the non-empty many-sorted over S) is non-empty (S) (S) (S) (S) (S) (S) (S) (S)
the Sorts of the non-empty many-sorted over S is Relation-like non-empty the carrier of S -defined Function-like V17( the carrier of S) set
the carrier of S is set
( the carrier of S, the Sorts of the non-empty many-sorted over S) is non empty functional with_common_domain ( the carrier of S, the Sorts of the non-empty many-sorted over S) ( the carrier of S, the Sorts of the non-empty many-sorted over S) ( the carrier of S, the Sorts of the non-empty many-sorted over S) ( the carrier of S, the Sorts of the non-empty many-sorted over S) ( the carrier of S, the Sorts of the non-empty many-sorted over S) ( the carrier of S, the Sorts of the non-empty many-sorted over S) Element of bool ( the carrier of S, the Sorts of the non-empty many-sorted over S)
( the carrier of S, the Sorts of the non-empty many-sorted over S) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of the non-empty many-sorted over S) is non empty set
(S, the Sorts of the non-empty many-sorted over S,( the carrier of S, the Sorts of the non-empty many-sorted over S)) is (S) (S)
S is 1-sorted
the carrier of S is set
D is (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the of D is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
S is 1-sorted
the carrier of S is set
D is (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the of D is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
S is 1-sorted
the carrier of S is set
D is (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the of D is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
S is 1-sorted
the carrier of S is set
D is (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the of D is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
S is 1-sorted
the carrier of S is set
D is (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the of D is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
S is 1-sorted
the carrier of S is set
D is (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the of D is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
S is 1-sorted
the carrier of S is set
D is Relation-like non-empty the carrier of S -defined Function-like V17( the carrier of S) set
( the carrier of S,D) is non empty functional with_common_domain set
bool ( the carrier of S,D) is non empty set
M is functional Element of bool ( the carrier of S,D)
(S,D,M) is (S) (S)
the Sorts of (S,D,M) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
S is 1-sorted
the carrier of S is set
D is many-sorted over S
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
M is functional ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
(S, the Sorts of D,M) is (S) (S)
S is 1-sorted
the carrier of S is set
D is many-sorted over S
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
M is non empty functional ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
(S, the Sorts of D,M) is (S) (S) (S)
S is 1-sorted
the carrier of S is set
D is many-sorted over S
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
M is functional ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
(S, the Sorts of D,M) is (S) (S)
S is 1-sorted
the carrier of S is set
D is many-sorted over S
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
M is non empty functional ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
(S, the Sorts of D,M) is (S) (S) (S)
S is 1-sorted
the carrier of S is set
D is many-sorted over S
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
M is non empty functional ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
(S, the Sorts of D,M) is (S) (S)
S is 1-sorted
the carrier of S is set
D is many-sorted over S
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
M is non empty functional ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
(S, the Sorts of D,M) is (S) (S)
S is 1-sorted
D is (S)
the carrier of S is set
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the of D is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
S is 1-sorted
D is (S)
the carrier of S is set
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the of D is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
S is 1-sorted
D is (S)
the carrier of S is set
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the of D is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
S is 1-sorted
D is (S)
the carrier of S is set
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the of D is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
S is set
S is 1-sorted
the carrier of S is set
D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
( the carrier of S,D) is non empty functional with_common_domain ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) Element of bool ( the carrier of S,D)
( the carrier of S,D) is non empty functional with_common_domain set
bool ( the carrier of S,D) is non empty set
[:( the carrier of S,D),( the carrier of S,D):] is non empty Relation-like set
bool [:( the carrier of S,D),( the carrier of S,D):] is non empty set
M is non empty Relation-like Function-like V17(( the carrier of S,D)) quasi_total ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) Element of bool [:( the carrier of S,D),( the carrier of S,D):]
{ b₁ where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S,D,( the carrier of S,D)) : ( the carrier of S,D,M,b₁) = b₁ } is set
{ b₁ where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S,D,( the carrier of S,D)) : S₁[b₁] } is set
bool ( the carrier of S,D) is non empty set
d is functional Element of bool ( the carrier of S,D)
(S,D,d) is (S) (S)
the Sorts of (S,D,d) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the of (S,D,d) is functional Element of bool ( the carrier of S, the Sorts of (S,D,d))
( the carrier of S, the Sorts of (S,D,d)) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of (S,D,d)) is non empty set
F is (S) (S)
the Sorts of F is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the of F is functional Element of bool ( the carrier of S, the Sorts of F)
( the carrier of S, the Sorts of F) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of F) is non empty set
d is (S) (S)
the Sorts of d is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the of d is functional Element of bool ( the carrier of S, the Sorts of d)
( the carrier of S, the Sorts of d) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of d) is non empty set
S is 1-sorted
the carrier of S is set
D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
( the carrier of S,D) is non empty functional with_common_domain ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) Element of bool ( the carrier of S,D)
( the carrier of S,D) is non empty functional with_common_domain set
bool ( the carrier of S,D) is non empty set
[:( the carrier of S,D),( the carrier of S,D):] is non empty Relation-like set
bool [:( the carrier of S,D),( the carrier of S,D):] is non empty set
M is non empty Relation-like Function-like V17(( the carrier of S,D)) quasi_total ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) Element of bool [:( the carrier of S,D),( the carrier of S,D):]
(S,D,M) is (S) (S)
the Sorts of (S,D,M) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
{ b₁ where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S,D,( the carrier of S,D)) : S₁[b₁] } is set
the of (S,D,M) is functional Element of bool ( the carrier of S, the Sorts of (S,D,M))
( the carrier of S, the Sorts of (S,D,M)) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of (S,D,M)) is non empty set
bool ( the carrier of S,D) is non empty set
d is functional Element of bool ( the carrier of S,D)
(S,D,d) is (S) (S)
f is functional Element of bool ( the carrier of S,D)
( the carrier of S,D,f) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool D
bool D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
meet ( the carrier of S,D,f) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of D
x is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
q is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S,D,( the carrier of S,D))
SF is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S,D,( the carrier of S,D))
( the carrier of S,D,M,q) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S,D,( the carrier of S,D))
SF9 is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S,D,( the carrier of S,D))
( the carrier of S,D,M,SF9) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S,D,( the carrier of S,D))
S is 1-sorted
the carrier of S is set
D is (S) (S) (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
( the carrier of S, the Sorts of D) is non empty functional with_common_domain ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
M is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D
the of D is non empty functional ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
{ b₁ where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : ( M c= b₁ & b₁ in the of D ) } is set
{ b₁ where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : S₁[b₁] } is set
bool ( the carrier of S, the Sorts of D) is non empty set
F is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D,F) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D
bool the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
meet ( the carrier of S, the Sorts of D,F) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D
d is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
F is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
f is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D,f) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D
bool the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
meet ( the carrier of S, the Sorts of D,f) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D
d is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
q is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D,q) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D
meet ( the carrier of S, the Sorts of D,q) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D
S is 1-sorted
the carrier of S is set
D is (S) (S) (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
( the carrier of S, the Sorts of D) is non empty functional with_common_domain ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
[:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):] is non empty Relation-like set
bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):] is non empty set
the of D is non empty functional ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
M is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
F is non empty Relation-like Function-like V17(( the carrier of S, the Sorts of D)) quasi_total Element of bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):]
( the carrier of S, the Sorts of D,F,M) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
(S,D,M) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
{ b₁ where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : ( M c= b₁ & b₁ in the of D ) } is set
d is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D,d) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D
bool the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
meet ( the carrier of S, the Sorts of D,d) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D
f is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
q is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
S is 1-sorted
the carrier of S is set
D is (S) (S) (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
( the carrier of S, the Sorts of D) is non empty functional with_common_domain ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
[:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):] is non empty Relation-like set
bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):] is non empty set
the of D is non empty functional ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
M is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
F is non empty Relation-like Function-like V17(( the carrier of S, the Sorts of D)) quasi_total Element of bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):]
( the carrier of S, the Sorts of D,F,M) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
{ H₁(b₁) where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : ( H₁(b₁) in the of D & S₁[b₁] ) } is set
q is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
x is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
{ H₁(b₁) where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : S₂[b₁] } is set
{ H₁(b₁) where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : S₃[b₁] } is set
(S,D,M) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
{ b₁ where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : ( M c= b₁ & b₁ in the of D ) } is set
q is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D,q) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D
bool the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
meet ( the carrier of S, the Sorts of D,q) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D
S is 1-sorted
the carrier of S is set
D is (S) (S) (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
( the carrier of S, the Sorts of D) is non empty functional with_common_domain ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
[:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):] is non empty Relation-like set
bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):] is non empty set
M is non empty Relation-like Function-like V17(( the carrier of S, the Sorts of D)) quasi_total Element of bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):]
d is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
( the carrier of S, the Sorts of D,M,d) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
(S,D,d) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
the of D is non empty functional ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
{ b₁ where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : ( d c= b₁ & b₁ in the of D ) } is set
f is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D,f) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D
bool the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
meet ( the carrier of S, the Sorts of D,f) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D
q is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
x is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
d is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
f is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
( the carrier of S, the Sorts of D,M,d) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
( the carrier of S, the Sorts of D,M,f) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
(S,D,f) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
the of D is non empty functional ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
{ b₁ where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : ( f c= b₁ & b₁ in the of D ) } is set
q is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D,q) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D
bool the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
meet ( the carrier of S, the Sorts of D,q) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D
(S,D,d) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
{ b₁ where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : ( d c= b₁ & b₁ in the of D ) } is set
x is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D,x) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D
meet ( the carrier of S, the Sorts of D,x) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D
SF is set
( the carrier of S, the Sorts of D,q) . SF is set
( the carrier of S, the Sorts of D,x) . SF is set
SF9 is set
i is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V45() Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D,i) is Relation-like empty-yielding the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D
( the carrier of S, the Sorts of D,i) . SF is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V45() set
{ (b₁ . SF) where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : b₁ in q } is set
i is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
i . SF is set
Q is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
Q is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
{ (b₁ . SF) where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : b₁ in x } is set
d is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
( the carrier of S, the Sorts of D,M,d) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
( the carrier of S, the Sorts of D,M,( the carrier of S, the Sorts of D,M,d)) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
(S,D,d) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
the of D is non empty functional ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
{ b₁ where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : ( d c= b₁ & b₁ in the of D ) } is set
f is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D,f) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D
bool the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
meet ( the carrier of S, the Sorts of D,f) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D
q is set
x is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
M . (meet ( the carrier of S, the Sorts of D,f)) is set
S is 1-sorted
the carrier of S is set
D is (S) (S) (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
( the carrier of S, the Sorts of D) is non empty functional with_common_domain ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
[:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):] is non empty Relation-like set
bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):] is non empty set
F is non empty Relation-like Function-like V17(( the carrier of S, the Sorts of D)) quasi_total Element of bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):]
d is non empty Relation-like Function-like V17(( the carrier of S, the Sorts of D)) quasi_total Element of bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):]
f is non empty Relation-like Function-like V17(( the carrier of S, the Sorts of D)) quasi_total ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):]
q is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
( the carrier of S, the Sorts of D,f,q) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
(S,D,q) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
M is non empty Relation-like Function-like V17(( the carrier of S, the Sorts of D)) quasi_total ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):]
F is non empty Relation-like Function-like V17(( the carrier of S, the Sorts of D)) quasi_total ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):]
dom M is non empty set
dom F is non empty set
f is set
M . f is set
q is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
(S,D,q) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
F . f is set
S is 1-sorted
the carrier of S is set
D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
( the carrier of S,D) is non empty functional with_common_domain ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) Element of bool ( the carrier of S,D)
( the carrier of S,D) is non empty functional with_common_domain set
bool ( the carrier of S,D) is non empty set
[:( the carrier of S,D),( the carrier of S,D):] is non empty Relation-like set
bool [:( the carrier of S,D),( the carrier of S,D):] is non empty set
M is non empty Relation-like Function-like V17(( the carrier of S,D)) quasi_total ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) Element of bool [:( the carrier of S,D),( the carrier of S,D):]
(S,D,M) is (S) (S) (S) (S) (S)
the Sorts of (S,D,M) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
( the carrier of S, the Sorts of (S,D,M)) is non empty functional with_common_domain ( the carrier of S, the Sorts of (S,D,M)) ( the carrier of S, the Sorts of (S,D,M)) ( the carrier of S, the Sorts of (S,D,M)) ( the carrier of S, the Sorts of (S,D,M)) ( the carrier of S, the Sorts of (S,D,M)) ( the carrier of S, the Sorts of (S,D,M)) Element of bool ( the carrier of S, the Sorts of (S,D,M))
( the carrier of S, the Sorts of (S,D,M)) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of (S,D,M)) is non empty set
(S,(S,D,M)) is non empty Relation-like Function-like V17(( the carrier of S, the Sorts of (S,D,M))) quasi_total ( the carrier of S, the Sorts of (S,D,M)) ( the carrier of S, the Sorts of (S,D,M)) ( the carrier of S, the Sorts of (S,D,M)) Element of bool [:( the carrier of S, the Sorts of (S,D,M)),( the carrier of S, the Sorts of (S,D,M)):]
[:( the carrier of S, the Sorts of (S,D,M)),( the carrier of S, the Sorts of (S,D,M)):] is non empty Relation-like set
bool [:( the carrier of S, the Sorts of (S,D,M)),( the carrier of S, the Sorts of (S,D,M)):] is non empty set
q is non empty Relation-like Function-like V17(( the carrier of S, the Sorts of (S,D,M))) quasi_total ( the carrier of S, the Sorts of (S,D,M)) ( the carrier of S, the Sorts of (S,D,M)) ( the carrier of S, the Sorts of (S,D,M)) Element of bool [:( the carrier of S, the Sorts of (S,D,M)),( the carrier of S, the Sorts of (S,D,M)):]
x is set
(S,(S,D,M)) . x is set
q . x is set
SF is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of (S,D,M),( the carrier of S, the Sorts of (S,D,M)))
(S,(S,D,M),SF) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of (S,D,M),( the carrier of S, the Sorts of (S,D,M)))
the of (S,D,M) is non empty functional ( the carrier of S, the Sorts of (S,D,M)) ( the carrier of S, the Sorts of (S,D,M)) ( the carrier of S, the Sorts of (S,D,M)) Element of bool ( the carrier of S, the Sorts of (S,D,M))
{ b₁ where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of (S,D,M),( the carrier of S, the Sorts of (S,D,M))) : ( SF c= b₁ & b₁ in the of (S,D,M) ) } is set
SF9 is functional Element of bool ( the carrier of S, the Sorts of (S,D,M))
( the carrier of S, the Sorts of (S,D,M),SF9) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of (S,D,M)
bool the Sorts of (S,D,M) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
meet ( the carrier of S, the Sorts of (S,D,M),SF9) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of (S,D,M)
( the carrier of S, the Sorts of (S,D,M),q,SF) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of (S,D,M),( the carrier of S, the Sorts of (S,D,M)))
Q is set
the Sorts of (S,D,M) . Q is set
bool ( the Sorts of (S,D,M) . Q) is non empty set
bool (bool ( the Sorts of (S,D,M) . Q)) is non empty set
( the carrier of S, the Sorts of (S,D,M),SF9) . Q is set
(meet ( the carrier of S, the Sorts of (S,D,M),SF9)) . Q is set
z is Element of bool (bool ( the Sorts of (S,D,M) . Q))
Intersect z is Element of bool ( the Sorts of (S,D,M) . Q)
i is non empty functional Element of bool ( the carrier of S, the Sorts of (S,D,M))
{ (b₁ . Q) where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of (S,D,M),( the carrier of S, the Sorts of (S,D,M))) : b₁ in i } is set
{ b₁ where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of (S,D,M),( the carrier of S, the Sorts of (S,D,M))) : ( the carrier of S, the Sorts of (S,D,M),q,b₁) = b₁ } is set
x is set
q is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of (S,D,M),( the carrier of S, the Sorts of (S,D,M)))
q . Q is set
X is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of (S,D,M),( the carrier of S, the Sorts of (S,D,M)))
( the carrier of S, the Sorts of (S,D,M),q,X) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of (S,D,M),( the carrier of S, the Sorts of (S,D,M)))
( the carrier of S, the Sorts of (S,D,M),q,SF) . Q is set
c₁₇ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of (S,D,M),( the carrier of S, the Sorts of (S,D,M)))
( the carrier of S, the Sorts of (S,D,M),q,c₁₇) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of (S,D,M),( the carrier of S, the Sorts of (S,D,M)))
( the carrier of S, the Sorts of (S,D,M),q,( the carrier of S, the Sorts of (S,D,M),q,SF)) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of (S,D,M),( the carrier of S, the Sorts of (S,D,M)))
( the carrier of S, the Sorts of (S,D,M),i) is Relation-like non-empty the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of (S,D,M)
( the carrier of S, the Sorts of (S,D,M),i) . Q is set
S is 1-sorted
D is (S) (S) (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the carrier of S is set
(S,D) is non empty Relation-like Function-like V17(( the carrier of S, the Sorts of D)) quasi_total ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):]
( the carrier of S, the Sorts of D) is non empty functional with_common_domain ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of D) is non empty set
[:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):] is non empty Relation-like set
bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):] is non empty set
(S, the Sorts of D,(S,D)) is (S) (S) (S) (S) (S)
the of D is non empty functional ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)
(S, the Sorts of D, the of D) is (S) (S) (S) (S) (S)
the of (S, the Sorts of D,(S,D)) is non empty functional ( the carrier of S, the Sorts of (S, the Sorts of D,(S,D))) ( the carrier of S, the Sorts of (S, the Sorts of D,(S,D))) ( the carrier of S, the Sorts of (S, the Sorts of D,(S,D))) Element of bool ( the carrier of S, the Sorts of (S, the Sorts of D,(S,D)))
the Sorts of (S, the Sorts of D,(S,D)) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
( the carrier of S, the Sorts of (S, the Sorts of D,(S,D))) is non empty functional with_common_domain set
bool ( the carrier of S, the Sorts of (S, the Sorts of D,(S,D))) is non empty set
{ b₁ where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : ( the carrier of S, the Sorts of D,(S,D),b₁) = b₁ } is set
q is set
x is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
(S,D,x) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
{ b₁ where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : ( x c= b₁ & b₁ in the of D ) } is set
SF is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D,SF) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D
bool the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
meet ( the carrier of S, the Sorts of D,SF) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D
i is set
the Sorts of D . i is set
bool ( the Sorts of D . i) is non empty set
bool (bool ( the Sorts of D . i)) is non empty set
SF9 is non empty functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D,SF9) is Relation-like non-empty the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D
( the carrier of S, the Sorts of D,SF9) . i is set
meet ( the carrier of S, the Sorts of D,SF9) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D
(meet ( the carrier of S, the Sorts of D,SF9)) . i is set
Q is Element of bool (bool ( the Sorts of D . i))
Intersect Q is Element of bool ( the Sorts of D . i)
{ (b₁ . i) where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : b₁ in SF9 } is set
x . i is set
z is set
x is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
x . i is set
q is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
( the carrier of S, the Sorts of D,(S,D),x) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
( the carrier of S, the Sorts of D,(S,D),x) . i is set
q is set
x is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
( the carrier of S, the Sorts of D,(S,D),x) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
{ H₁(b₁) where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : ( H₁(b₁) in the of D & S₃[b₁] ) } is set
SF is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
SF9 is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
{ H₁(b₁) where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : S₂[b₁] } is set
{ H₁(b₁) where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : S₁[b₁] } is set
(S,D,x) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))
{ b₁ where b₁ is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D)) : ( x c= b₁ & b₁ in the of D ) } is set
SF is functional Element of bool ( the carrier of S, the Sorts of D)
( the carrier of S, the Sorts of D,SF) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D
bool the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
meet ( the carrier of S, the Sorts of D,SF) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D