:: CLOSURE3 semantic presentation

K164() is Element of bool K160()

K160() is set

bool K160() is non empty set

K137() is set

bool K137() is non empty set

bool K164() is non empty set

K161() is set

K162() is set

K163() is set

2 is non empty set

{} is empty Function-like functional finite V45() V87() set

the empty Function-like functional finite V45() V87() set is empty Function-like functional finite V45() V87() set

1 is non empty set

3 is non empty set

K165() is empty Function-like functional finite V45() V87() Element of K164()

S is non empty 1-sorted

the carrier of S is non empty set

1-sorted(# the carrier of S #) is strict 1-sorted

S is non empty set

MA is non empty Relation-like S -defined Function-like V17(S) set

I is non empty Relation-like S -defined Function-like V17(S) set

MA +* I is Relation-like Function-like set

dom MA is set

dom I is set

S is set

MA is Relation-like S -defined Function-like V17(S) set

Bool MA is non empty functional with_common_domain set

bool (Bool MA) is non empty set

I is Relation-like S -defined Function-like V17(S) set

SS is functional Element of bool (Bool MA)

|:SS:| is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool MA

bool MA is Relation-like S -defined Function-like V17(S) set

meet |:SS:| is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

S is non empty non void V62() ManySortedSign

the carrier of S is non empty set

MA is strict non-empty MSAlgebra over S

the Sorts of MA is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set

Bool the Sorts of MA is non empty functional with_common_domain set

bool (Bool the Sorts of MA) is non empty set

SubSort MA is set

I is functional Element of bool (Bool the Sorts of MA)

|:I:| is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of MA

bool the Sorts of MA is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

meet |:I:| is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of MA

SS is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of MA

x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of MA

[[0]] the carrier of S is non empty Relation-like non non-empty empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set

the carrier of S --> {} is non empty Relation-like the carrier of S -defined {{}} -valued Function-like V17( the carrier of S) quasi_total Element of bool [: the carrier of S,{{}}:]

{{}} is non empty finite V45() set

[: the carrier of S,{{}}:] is non empty set

bool [: the carrier of S,{{}}:] is non empty set

the carrier' of S is non empty set

A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of MA

y is Element of the carrier' of S

the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is non empty set

bool [: the carrier' of S, the carrier of S:] is non empty set

the ResultSort of S . y is Element of the carrier of S

the_result_sort_of y is Element of the carrier of S

dom the ResultSort of S is set

Result (y,MA) is non empty Element of rng the Sorts of MA

rng the Sorts of MA is with_non-empty_elements set

the ResultSort of S * A is Relation-like Function-like set

( the ResultSort of S * A) . y is set

A . (the_result_sort_of y) is set

Args (y,MA) is non empty Element of rng ( the Sorts of MA #)

the Sorts of MA # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the carrier of S * is non empty functional V87() M12( the carrier of S)

rng ( the Sorts of MA #) is set

Den (y,MA) is non empty Relation-like Args (y,MA) -defined Result (y,MA) -valued Function-like V17( Args (y,MA)) quasi_total Element of bool [:(Args (y,MA)),(Result (y,MA)):]

[:(Args (y,MA)),(Result (y,MA)):] is non empty set

bool [:(Args (y,MA)),(Result (y,MA)):] is non empty set

A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the_arity_of y is Relation-like K164() -defined the carrier of S -valued Function-like finite V85() V86() Element of the carrier of S *

(A #) . (the_arity_of y) is set

(Den (y,MA)) | ((A #) . (the_arity_of y)) is Relation-like Args (y,MA) -defined Result (y,MA) -valued Function-like Element of bool [:(Args (y,MA)),(Result (y,MA)):]

rng ((Den (y,MA)) | ((A #) . (the_arity_of y))) is set

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]

[: the carrier' of S,( the carrier of S *):] is non empty set

bool [: the carrier' of S,( the carrier of S *):] is non empty set

the Arity of S . y is Relation-like K164() -defined Function-like finite V85() V86() Element of the carrier of S *

dom the Arity of S is set

the Arity of S * (A #) is Relation-like Function-like set

( the Arity of S * (A #)) . y is set

the carrier' of S is non empty set

x is Element of the carrier' of S

the_result_sort_of x is Element of the carrier of S

the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is non empty set

bool [: the carrier' of S, the carrier of S:] is non empty set

the ResultSort of S . x is Element of the carrier of S

dom the ResultSort of S is set

the carrier of S * is non empty functional V87() M12( the carrier of S)

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]

[: the carrier' of S,( the carrier of S *):] is non empty set

bool [: the carrier' of S,( the carrier of S *):] is non empty set

the Arity of S . x is Relation-like K164() -defined Function-like finite V85() V86() Element of the carrier of S *

the_arity_of x is Relation-like K164() -defined the carrier of S -valued Function-like finite V85() V86() Element of the carrier of S *

dom the Arity of S is set

SS # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * (SS #) is Relation-like Function-like set

( the Arity of S * (SS #)) . x is set

(SS #) . (the_arity_of x) is set

Result (x,MA) is non empty Element of rng the Sorts of MA

rng the Sorts of MA is with_non-empty_elements set

the ResultSort of S * the Sorts of MA is Relation-like Function-like set

( the ResultSort of S * the Sorts of MA) . x is set

the Sorts of MA . (the_result_sort_of x) is non empty set

Args (x,MA) is non empty Element of rng ( the Sorts of MA #)

the Sorts of MA # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

rng ( the Sorts of MA #) is set

Den (x,MA) is non empty Relation-like Args (x,MA) -defined Result (x,MA) -valued Function-like V17( Args (x,MA)) quasi_total Element of bool [:(Args (x,MA)),(Result (x,MA)):]

[:(Args (x,MA)),(Result (x,MA)):] is non empty set

bool [:(Args (x,MA)),(Result (x,MA)):] is non empty set

(Den (x,MA)) | ((SS #) . (the_arity_of x)) is Relation-like Args (x,MA) -defined Result (x,MA) -valued Function-like Element of bool [:(Args (x,MA)),(Result (x,MA)):]

rng ((Den (x,MA)) | ((SS #) . (the_arity_of x))) is set

SS . (the_result_sort_of x) is set

bool ( the Sorts of MA . (the_result_sort_of x)) is non empty set

bool (bool ( the Sorts of MA . (the_result_sort_of x))) is non empty set

|:I:| . (the_result_sort_of x) is Element of bool (bool ( the Sorts of MA . (the_result_sort_of x)))

A is Element of bool (bool ( the Sorts of MA . (the_result_sort_of x)))

Intersect A is Element of bool ( the Sorts of MA . (the_result_sort_of x))

y is set

dom ((Den (x,MA)) | ((SS #) . (the_arity_of x))) is set

z is set

((Den (x,MA)) | ((SS #) . (the_arity_of x))) . z is set

Bool the Sorts of MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool the Sorts of MA)

{ (b

i is set

SS9 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) Element of Bool the Sorts of MA

SS9 . (the_result_sort_of x) is set

SS9 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of MA

SS9 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * (SS9 #) is Relation-like Function-like set

( the Arity of S * (SS9 #)) . x is set

(Den (x,MA)) | (( the Arity of S * (SS9 #)) . x) is Relation-like Args (x,MA) -defined Result (x,MA) -valued Function-like Element of bool [:(Args (x,MA)),(Result (x,MA)):]

rng ((Den (x,MA)) | (( the Arity of S * (SS9 #)) . x)) is set

the ResultSort of S * SS9 is Relation-like Function-like set

( the ResultSort of S * SS9) . x is set

(Den (x,MA)) | (( the Arity of S * (SS #)) . x) is Relation-like Args (x,MA) -defined Result (x,MA) -valued Function-like Element of bool [:(Args (x,MA)),(Result (x,MA)):]

dom ((Den (x,MA)) | (( the Arity of S * (SS #)) . x)) is set

dom ((Den (x,MA)) | (( the Arity of S * (SS9 #)) . x)) is set

(Den (x,MA)) . z is set

((Den (x,MA)) | (( the Arity of S * (SS9 #)) . x)) . z is set

SS9 . ( the ResultSort of S . x) is set

SS9 . (the_result_sort_of x) is set

the ResultSort of S * SS is Relation-like Function-like set

( the ResultSort of S * SS) . x is set

MA is set

S is set

I is set

SS is set

M is set

x is set

S is non empty set

MA is non empty Relation-like S -defined Function-like V17(S) set

{ b

support MA is set

SS is set

dom MA is set

MA . SS is set

SS is set

M is Element of S

MA . M is set

S is non empty set

MA is non empty Relation-like S -defined Function-like V17(S) set

support MA is set

{ b

I is set

SS is set

S is non empty set

[[0]] S is non empty Relation-like non non-empty empty-yielding S -defined Function-like V17(S) set

S --> {} is non empty Relation-like S -defined {{}} -valued Function-like V17(S) quasi_total Element of bool [:S,{{}}:]

{{}} is non empty finite V45() set

[:S,{{}}:] is non empty set

bool [:S,{{}}:] is non empty set

MA is non empty Relation-like non-empty non empty-yielding S -defined Function-like V17(S) set

(S,MA) is set

{ b

MA | (S,MA) is Relation-like Function-like set

([[0]] S) +* (MA | (S,MA)) is Relation-like Function-like set

SS is set

MA . SS is set

dom MA is set

S is non empty set

MA is non empty Relation-like non-empty non empty-yielding S -defined Function-like V17(S) set

(S,MA) is set

{ b

MA | (S,MA) is Relation-like Function-like set

I is non empty Relation-like non-empty non empty-yielding S -defined Function-like V17(S) set

(S,I) is set

{ b

I | (S,I) is Relation-like Function-like set

dom MA is set

dom I is set

SS is set

MA . SS is set

I . SS is set

dom (I | (S,I)) is set

(dom I) /\ (S,I) is set

dom (MA | (S,MA)) is set

(dom MA) /\ (S,MA) is set

(I | (S,I)) . SS is set

S is non empty set

MA is non empty Relation-like S -defined Function-like V17(S) set

Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)

Bool MA is non empty functional with_common_domain set

bool (Bool MA) is non empty set

I is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

SS is Element of S

I . SS is set

M is set

{SS} is non empty finite set

{M} is non empty finite set

{SS} --> {M} is non empty Relation-like {SS} -defined {{M}} -valued Function-like V17({SS}) quasi_total finite Element of bool [:{SS},{{M}}:]

{{M}} is non empty finite V45() set

[:{SS},{{M}}:] is non empty finite set

bool [:{SS},{{M}}:] is non empty finite V45() set

[[0]] S is non empty Relation-like non non-empty empty-yielding S -defined Function-like V17(S) set

S --> {} is non empty Relation-like S -defined {{}} -valued Function-like V17(S) quasi_total Element of bool [:S,{{}}:]

{{}} is non empty finite V45() set

[:S,{{}}:] is non empty set

bool [:S,{{}}:] is non empty set

([[0]] S) +* ({SS} --> {M}) is Relation-like Function-like set

dom ({SS} --> {M}) is finite set

({SS} --> {M}) . SS is set

(([[0]] S) +* ({SS} --> {M})) . SS is set

dom (([[0]] S) +* ({SS} --> {M})) is set

dom ([[0]] S) is set

(dom ([[0]] S)) \/ (dom ({SS} --> {M})) is set

S \/ {SS} is non empty set

A is non empty Relation-like S -defined Function-like V17(S) set

y is set

A . y is set

MA . y is set

i is set

z is non empty Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

z . y is set

(S --> {}) . y is set

y is non empty Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

z is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

i is set

z . i is set

I . i is set

SS9 is set

(S --> {}) . i is set

{ b

i is set

SS9 is Element of S

z . SS9 is set

SS9 is Element of S

dom z is set

z . SS9 is set

(S --> {}) . SS9 is finite Element of {{}}

SS9 is Element of S

z . SS9 is set

i is set

SS9 is Element of S

z . SS9 is set

z . SS is set

(S,z) is set

i is set

z . i is set

(S --> {}) . i is set

S is set

MA is Relation-like S -defined Function-like V17(S) set

Bool MA is non empty functional with_common_domain set

bool (Bool MA) is non empty set

Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)

I is functional Element of bool (Bool MA)

{ (b

union { (b

SS is set

{ (b

union { (b

SS is Relation-like Function-like set

dom SS is set

M is Relation-like S -defined Function-like V17(S) set

x is set

M . x is set

MA . x is set

A is set

{ (b

union { (b

A is set

y is Relation-like S -defined Function-like V17(S) Element of Bool MA

y . x is set

z is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

z . x is set

x is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

A is set

x . A is set

{ (b

union { (b

SS is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

M is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

x is set

SS . x is set

M . x is set

{ (b

union { (b

S is set

MA is Relation-like S -defined Function-like V17(S) set

Bool MA is non empty functional with_common_domain set

bool (Bool MA) is non empty set

I is empty proper Function-like functional finite V45() V87() Element of bool (Bool MA)

(S,MA,I) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

SS is set

(S,MA,I) . SS is set

Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)

{ (b

union { (b

x is set

A is set

A is Relation-like S -defined Function-like V17(S) Element of Bool MA

A . SS is set

S is set

MA is Relation-like S -defined Function-like V17(S) set

Bool MA is non empty functional with_common_domain set

bool (Bool MA) is non empty set

I is functional Element of bool (Bool MA)

(S,MA,I) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

|:I:| is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool MA

bool MA is Relation-like S -defined Function-like V17(S) set

union |:I:| is Relation-like S -defined Function-like V17(S) set

M is Relation-like S -defined Function-like V17(S) set

x is set

(S,MA,I) . x is set

M . x is set

|:I:| . x is set

Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)

{ (b

union (|:I:| . x) is set

M is Relation-like S -defined Function-like V17(S) set

x is set

(S,MA,I) . x is set

M . x is set

[[0]] S is Relation-like empty-yielding S -defined Function-like V17(S) set

S --> {} is Relation-like S -defined {{}} -valued Function-like V17(S) quasi_total Element of bool [:S,{{}}:]

{{}} is non empty finite V45() set

[:S,{{}}:] is set

bool [:S,{{}}:] is non empty set

S is set

MA is Relation-like S -defined Function-like V17(S) set

Bool MA is non empty functional with_common_domain set

bool (Bool MA) is non empty set

I is functional Element of bool (Bool MA)

SS is functional Element of bool (Bool MA)

I \/ SS is set

S is set

MA is Relation-like S -defined Function-like V17(S) set

Bool MA is non empty functional with_common_domain set

bool (Bool MA) is non empty set

I is functional Element of bool (Bool MA)

SS is functional Element of bool (Bool MA)

(S,MA,I,SS) is functional Element of bool (Bool MA)

(S,MA,(S,MA,I,SS)) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

(S,MA,I) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

(S,MA,SS) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

(S,MA,I) \/ (S,MA,SS) is Relation-like S -defined Function-like V17(S) set

M is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

A is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

y is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

x is Relation-like S -defined Function-like V17(S) set

A is Relation-like S -defined Function-like V17(S) set

z is Relation-like S -defined Function-like V17(S) set

A \/ z is Relation-like S -defined Function-like V17(S) set

i is set

x . i is set

(A \/ z) . i is set

Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)

{ (b

union { (b

A . i is set

z . i is set

(A . i) \/ (z . i) is set

SS9 is set

{ (b

union { (b

SS9 is set

v is Relation-like S -defined Function-like V17(S) Element of Bool MA

v . i is set

{ (b

union { (b

SS9 is set

v is Relation-like S -defined Function-like V17(S) Element of Bool MA

v . i is set

{ (b

union { (b

{ (b

union { (b

{ (b

union { (b

{ (b

union { (b

SS9 is set

SS9 is set

v is Relation-like S -defined Function-like V17(S) Element of Bool MA

v . i is set

S is set

MA is Relation-like S -defined Function-like V17(S) set

Bool MA is non empty functional with_common_domain set

bool (Bool MA) is non empty set

I is functional Element of bool (Bool MA)

SS is functional Element of bool (Bool MA)

(S,MA,I) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

(S,MA,SS) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

M is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

A is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

x is Relation-like S -defined Function-like V17(S) set

A is Relation-like S -defined Function-like V17(S) set

y is set

x . y is set

A . y is set

Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)

{ (b

union { (b

z is set

i is set

{ (b

SS9 is Relation-like S -defined Function-like V17(S) Element of Bool MA

SS9 . y is set

union { (b

S is set

MA is Relation-like S -defined Function-like V17(S) set

Bool MA is non empty functional with_common_domain set

bool (Bool MA) is non empty set

I is functional Element of bool (Bool MA)

SS is functional Element of bool (Bool MA)

I /\ SS is set

S is set

MA is Relation-like S -defined Function-like V17(S) set

Bool MA is non empty functional with_common_domain set

bool (Bool MA) is non empty set

I is functional Element of bool (Bool MA)

SS is functional Element of bool (Bool MA)

(S,MA,I,SS) is functional Element of bool (Bool MA)

(S,MA,(S,MA,I,SS)) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

(S,MA,I) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

(S,MA,SS) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

(S,MA,I) /\ (S,MA,SS) is Relation-like S -defined Function-like V17(S) set

M is Relation-like S -defined Function-like V17(S) set

x is Relation-like S -defined Function-like V17(S) set

A is Relation-like S -defined Function-like V17(S) set

x /\ A is Relation-like S -defined Function-like V17(S) set

A is set

M . A is set

(x /\ A) . A is set

x . A is set

Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)

{ (b

union { (b

A . A is set

{ (b

union { (b

{ (b

union { (b

y is set

z is set

i is Relation-like S -defined Function-like V17(S) Element of Bool MA

i . A is set

(x . A) /\ (A . A) is set

S is set

MA is Relation-like S -defined Function-like V17(S) set

Bool MA is non empty functional with_common_domain set

bool (Bool MA) is non empty set

I is set

{ (S,MA,b

union I is set

M is functional Element of bool (Bool MA)

SS is functional Element of bool (Bool MA)

(S,MA,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

(S,MA,SS) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

x is set

(S,MA,M) . x is set

(S,MA,SS) . x is set

A is set

Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)

{ (b

union { (b

A is set

y is Relation-like S -defined Function-like V17(S) Element of Bool MA

y . x is set

z is functional Element of bool (Bool MA)

(S,MA,z) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

(S,MA,z) . x is set

{ (b

union { (b

i is set

SS9 is Relation-like S -defined Function-like V17(S) Element of Bool MA

SS9 . x is set

{ (b

union { (b

A is set

Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)

{ (b

union { (b

A is set

y is Relation-like S -defined Function-like V17(S) Element of Bool MA

y . x is set

z is set

i is functional Element of bool (Bool MA)

{ (b

union { (b

(S,MA,i) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

(S,MA,i) . x is set

SS9 is set

{ (b

union { (b

S is non empty set

MA is non empty Relation-like S -defined Function-like V17(S) set

Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)

Bool MA is non empty functional with_common_domain set

bool (Bool MA) is non empty set

[:(Bool MA),(Bool MA):] is non empty set

bool [:(Bool MA),(Bool MA):] is non empty set

S is non empty set

MA is non empty Relation-like S -defined Function-like V17(S) set

Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)

Bool MA is non empty functional with_common_domain set

bool (Bool MA) is non empty set

[:(Bool MA),(Bool MA):] is non empty set

bool [:(Bool MA),(Bool MA):] is non empty set

id (Bool MA) is non empty Relation-like Bool MA -defined Bool MA -valued Function-like one-to-one V17( Bool MA) quasi_total Element of bool [:(Bool MA),(Bool MA):]

I is non empty Relation-like Bool MA -defined Bool MA -valued Function-like V17( Bool MA) quasi_total Element of bool [:(Bool MA),(Bool MA):]

SS is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

I . SS is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

{ (I . b

x is set

A is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

I . A is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

(S,A) is set

{ b

x is functional Element of bool (Bool MA)

(S,MA,x) is non empty Relation-like S -defined Function-like V17(S) ManySortedSubset of MA

A is Element of S

SS . A is set

(S,MA,x) . A is set

A is set

y is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

y . A is set

(S,y) is set

{ b

I . y is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

{ (b

union { (b

A is set

{ (b

union { (b

y is set

z is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

z . A is set

i is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

I . i is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

(S,i) is set

{ b

SS is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

I . SS is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

SS is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

M is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

I . SS is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

I . M is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

SS is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

I . SS is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

I . (I . SS) is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA

S is non empty 1-sorted

S is non empty non void V62() ManySortedSign

the carrier of S is non empty set

1-sorted(# the carrier of S #) is strict non empty 1-sorted

MA is non-empty MSAlgebra over S

the Sorts of MA is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set

SubSort MA is set

the carrier of 1-sorted(# the carrier of S #) is non empty set

Bool the Sorts of MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool the Sorts of MA)

Bool the Sorts of MA is non empty functional with_common_domain set

bool (Bool the Sorts of MA) is non empty set

SS is set

I is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) set

Bool I is non empty functional with_common_domain set

bool (Bool I) is non empty set

SS is functional Element of bool (Bool I)

ClosureStr(# I,SS #) is strict ClosureStr over 1-sorted(# the carrier of S #)

the Sorts of ClosureStr(# I,SS #) is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) set

the Family of ClosureStr(# I,SS #) is functional Element of bool (Bool the Sorts of ClosureStr(# I,SS #))

Bool the Sorts of ClosureStr(# I,SS #) is non empty functional with_common_domain set

bool (Bool the Sorts of ClosureStr(# I,SS #)) is non empty set

I is strict ClosureStr over 1-sorted(# the carrier of S #)

the Sorts of I is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) set

the carrier of 1-sorted(# the carrier of S #) is non empty set

the Family of I is functional Element of bool (Bool the Sorts of I)

Bool the Sorts of I is non empty functional with_common_domain set

bool (Bool the Sorts of I) is non empty set

SS is strict ClosureStr over 1-sorted(# the carrier of S #)

the Sorts of SS is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) set

the Family of SS is functional Element of bool (Bool the Sorts of SS)

Bool the Sorts of SS is non empty functional with_common_domain set

bool (Bool the Sorts of SS) is non empty set

S is non empty non void V62() ManySortedSign

the carrier of S is non empty set

MA is strict non-empty MSAlgebra over S

SubSort MA is set

the Sorts of MA is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set

Bool the Sorts of MA is non empty functional with_common_domain set

bool (Bool the Sorts of MA) is non empty set

Bool the Sorts of MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool the Sorts of MA)

I is set

I is functional Element of bool (Bool the Sorts of MA)

Union the Sorts of MA is set

bool (Union the Sorts of MA) is non empty Element of bool (bool (Union the Sorts of MA))

bool (Union the Sorts of MA) is non empty set

bool (bool (Union the Sorts of MA)) is non empty set

x is functional Element of bool (Bool the Sorts of MA)

|:x:| is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of MA

bool the Sorts of MA is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

meet |:x:| is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of MA

dom (meet |:x:|) is set

rng (meet |:x:|) is set

A is set

y is set

(meet |:x:|) . y is set

dom the Sorts of MA is set

the Sorts of MA . y is set

rng the Sorts of MA is with_non-empty_elements set

union (rng the Sorts of MA) is set

bool ( the Sorts of MA . y) is non empty set

bool (bool ( the Sorts of MA . y)) is non empty set

|:x:| . y is set

z is Element of bool (bool ( the Sorts of MA . y))

Intersect z is Element of bool ( the Sorts of MA . y)

bool (union (rng the Sorts of MA)) is non empty Element of bool (bool (union (rng the Sorts of MA)))

bool (union (rng the Sorts of MA)) is non empty set

bool (bool (union (rng the Sorts of MA))) is non empty set

Funcs ( the carrier of S,(bool (Union the Sorts of MA))) is non empty functional FUNCTION_DOMAIN of the carrier of S, bool (Union the Sorts of MA)

A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of MA

y is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of MA

S is non empty non void V62() ManySortedSign

the carrier of S is non empty set

1-sorted(# the carrier of S #) is strict non empty 1-sorted

MA is strict non-empty MSAlgebra over S

(S,MA) is strict ClosureStr over 1-sorted(# the carrier of S #)

the Sorts of MA is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set

Bool the Sorts of MA is non empty functional with_common_domain set

bool (Bool the Sorts of MA) is non empty set

SubSort MA is set

the Family of (S,MA) is functional Element of bool (Bool the Sorts of (S,MA))

the carrier of 1-sorted(# the carrier of S #) is non empty set

the Sorts of (S,MA) is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) set

Bool the Sorts of (S,MA) is non empty functional with_common_domain set

bool (Bool the Sorts of (S,MA)) is non empty set

I is non empty functional multiplicative absolutely-multiplicative properly-upper-bound Element of bool (Bool the Sorts of MA)

S is non empty non void V62() ManySortedSign

the carrier of S is non empty set

1-sorted(# the carrier of S #) is strict non empty 1-sorted

MA is strict non-empty MSAlgebra over S

(S,MA) is strict multiplicative absolutely-multiplicative properly-upper-bound ClosureStr over 1-sorted(# the carrier of S #)

ClSys->ClOp (S,MA) is non empty Relation-like Bool the Sorts of (S,MA) -defined Bool the Sorts of (S,MA) -valued Function-like V17( Bool the Sorts of (S,MA)) quasi_total reflexive monotonic idempotent Element of bool [:(Bool the Sorts of (S,MA)),(Bool the Sorts of (S,MA)):]

the carrier of 1-sorted(# the carrier of S #) is non empty set

the Sorts of (S,MA) is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) set

Bool the Sorts of (S,MA) is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool the Sorts of (S,MA))

Bool the Sorts of (S,MA) is non empty functional with_common_domain set

bool (Bool the Sorts of (S,MA)) is non empty set

[:(Bool the Sorts of (S,MA)),(Bool the Sorts of (S,MA)):] is non empty set

bool [:(Bool the Sorts of (S,MA)),(Bool the Sorts of (S,MA)):] is non empty set

x is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)

(ClSys->ClOp (S,MA)) . x is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)

{ ((ClSys->ClOp (S,MA)) . b

A is set

z is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)

(ClSys->ClOp (S,MA)) . z is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)

( the carrier of 1-sorted(# the carrier of S #),z) is set

{ b

y is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)

A is functional Element of bool (Bool the Sorts of (S,MA))

( the carrier of 1-sorted(# the carrier of S #), the Sorts of (S,MA),A) is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) ManySortedSubset of the Sorts of (S,MA)

y is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

z is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

i is Element of the carrier of S

y . i is set

z . i is set

SS9 is set

v is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)

v . i is set

( the carrier of 1-sorted(# the carrier of S #),v) is set

{ b

SS9 is non empty Relation-like Bool the Sorts of (S,MA) -defined Bool the Sorts of (S,MA) -valued Function-like V17( Bool the Sorts of (S,MA)) quasi_total reflexive Element of bool [:(Bool the Sorts of (S,MA)),(Bool the Sorts of (S,MA)):]

SS9 . v is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)

(SS9 . v) . i is set

(ClSys->ClOp (S,MA)) . v is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)

{ (b

union { (b

v is set

{ (b

union { (b

Y is set

ff is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)

ff . i is set

a is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)

(ClSys->ClOp (S,MA)) . a is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)

( the carrier of 1-sorted(# the carrier of S #),a) is set

{ b

SS9 is non empty Relation-like Bool the Sorts of (S,MA) -defined Bool the Sorts of (S,MA) -valued Function-like V17( Bool the Sorts of (S,MA)) quasi_total monotonic Element of bool [:(Bool the Sorts of (S,MA)),(Bool the Sorts of (S,MA)):]

SS9 . a is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)

SS9 . x is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)

x . i is set