:: MSUALG_5 semantic presentation

REAL is set

NAT is non empty V27() V28() V29() V50() V55() V56() Element of bool REAL

bool REAL is non empty set

COMPLEX is set

NAT is non empty V27() V28() V29() V50() V55() V56() set

bool NAT is non empty V50() set

[:NAT,NAT:] is Relation-like non empty V50() set

[:[:NAT,NAT:],NAT:] is Relation-like non empty V50() set

bool [:[:NAT,NAT:],NAT:] is non empty V50() set

Nat_Lattice is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr

the carrier of Nat_Lattice is non empty set

bool NAT is non empty V50() set

NATPLUS is non empty Element of bool NAT

[:NATPLUS,NATPLUS:] is Relation-like non empty set

[:[:NATPLUS,NATPLUS:],NATPLUS:] is Relation-like non empty set

bool [:[:NATPLUS,NATPLUS:],NATPLUS:] is non empty set

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non negative V27() V28() V29() V31() V32() V33() V34() V35() reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive V50() V55() V57( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set

1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT

2 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT

3 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT

Seg 1 is non empty trivial V50() V57(1) Element of bool NAT

{1} is non empty trivial V57(1) set

Seg 2 is non empty V50() V57(2) Element of bool NAT

{1,2} is non empty set

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non negative V27() V28() V29() V31() V32() V33() V34() V35() reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive V50() V55() V57( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

x is set

[:x,x:] is Relation-like set

bool [:x,x:] is non empty set

X is Relation-like Element of bool [:x,x:]

K is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

K is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

x is set

[:x,x:] is Relation-like set

bool [:x,x:] is non empty set

X is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

K is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

X "\/" K is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

X \/ K is Relation-like reflexive symmetric Element of bool [:x,x:]

(x,(X \/ K)) is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

K is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

x is set

[:x,x:] is Relation-like set

bool [:x,x:] is non empty set

X is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

(x,X) is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

K is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

x is set

[:x,x:] is Relation-like set

bool [:x,x:] is non empty set

{ b

id x is Relation-like x -defined x -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:x,x:]

K is non empty set

K is Element of K

a is Element of K

K \/ a is set

i is Relation-like Element of bool [:x,x:]

i9 is Relation-like Element of bool [:x,x:]

K9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

a9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

K9 \/ a9 is Relation-like reflexive symmetric Element of bool [:x,x:]

i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

i9 is Element of K

K2 is Element of K

y9 is Relation-like Element of bool [:x,x:]

a2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

[:K,K:] is Relation-like non empty set

[:[:K,K:],K:] is Relation-like non empty set

bool [:[:K,K:],K:] is non empty set

K is Relation-like Function-like V18([:K,K:],K) Element of bool [:[:K,K:],K:]

a is Element of K

K9 is Element of K

a /\ K9 is set

i9 is Relation-like Element of bool [:x,x:]

K2 is Relation-like Element of bool [:x,x:]

a9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

a9 /\ i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

K2 is Element of K

a is Relation-like Function-like V18([:K,K:],K) Element of bool [:[:K,K:],K:]

LattStr(# K,K,a #) is non empty strict LattStr

i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

a9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

i9 is Element of K

K2 is Element of K

K . (i9,K2) is Element of K

[i9,K2] is set

K . [i9,K2] is set

a2 is Element of K

n is Relation-like Element of bool [:x,x:]

i9 \/ K2 is set

n is Element of K

a9 \/ i is Relation-like reflexive symmetric Element of bool [:x,x:]

n is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

L is Element of K

K . (a9,i) is set

[a9,i] is set

K . [a9,i] is set

y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

a9 "\/" i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

i is Element of K

i9 is Element of K

a9 is Element of K

n is Relation-like Element of bool [:x,x:]

L is Relation-like Element of bool [:x,x:]

L is Relation-like Element of bool [:x,x:]

K . (i,i9) is Element of K

[i,i9] is set

K . [i,i9] is set

K . (a9,(K . (i,i9))) is Element of K

[a9,(K . (i,i9))] is set

K . [a9,(K . (i,i9))] is set

a2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

a2 "\/" y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

K . (a9,(a2 "\/" y9)) is set

[a9,(a2 "\/" y9)] is set

K . [a9,(a2 "\/" y9)] is set

K2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

K2 "\/" (a2 "\/" y9) is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

K2 "\/" a2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

(K2 "\/" a2) "\/" y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

K . ((K2 "\/" a2),i9) is set

[(K2 "\/" a2),i9] is set

K . [(K2 "\/" a2),i9] is set

K . (a9,i) is Element of K

[a9,i] is set

K . [a9,i] is set

K . ((K . (a9,i)),i9) is Element of K

[(K . (a9,i)),i9] is set

K . [(K . (a9,i)),i9] is set

K9 is non empty LattStr

the carrier of K9 is non empty set

a9 is Element of the carrier of K9

i is Element of the carrier of K9

i9 is Element of the carrier of K9

i "\/" i9 is Element of the carrier of K9

a9 "\/" (i "\/" i9) is Element of the carrier of K9

a9 "\/" i is Element of the carrier of K9

(a9 "\/" i) "\/" i9 is Element of the carrier of K9

the L_join of K9 is Relation-like Function-like V18([: the carrier of K9, the carrier of K9:], the carrier of K9) Element of bool [:[: the carrier of K9, the carrier of K9:], the carrier of K9:]

[: the carrier of K9, the carrier of K9:] is Relation-like non empty set

[:[: the carrier of K9, the carrier of K9:], the carrier of K9:] is Relation-like non empty set

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

the L_join of K9 . (a9,i) is Element of the carrier of K9

[a9,i] is set

the L_join of K9 . [a9,i] is set

the L_join of K9 . (a9,(i "\/" i9)) is Element of the carrier of K9

[a9,(i "\/" i9)] is set

the L_join of K9 . [a9,(i "\/" i9)] is set

K2 is Element of K

a2 is Element of K

y9 is Element of K

K . (a2,y9) is Element of K

[a2,y9] is set

K . [a2,y9] is set

K . (K2,(K . (a2,y9))) is Element of K

[K2,(K . (a2,y9))] is set

K . [K2,(K . (a2,y9))] is set

the L_join of K9 . (( the L_join of K9 . (a9,i)),i9) is Element of the carrier of K9

[( the L_join of K9 . (a9,i)),i9] is set

the L_join of K9 . [( the L_join of K9 . (a9,i)),i9] is set

i is Element of K

a9 is Element of K

a2 is Relation-like Element of bool [:x,x:]

y9 is Relation-like Element of bool [:x,x:]

K . (a9,i) is Element of K

[a9,i] is set

K . [a9,i] is set

K2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

i9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

K2 "\/" i9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

K . (i,a9) is Element of K

[i,a9] is set

K . [i,a9] is set

a9 is Element of the carrier of K9

i is Element of the carrier of K9

a9 "\/" i is Element of the carrier of K9

i "\/" a9 is Element of the carrier of K9

i9 is Element of K

K2 is Element of K

K . (i9,K2) is Element of K

[i9,K2] is set

K . [i9,K2] is set

the L_join of K9 is Relation-like Function-like V18([: the carrier of K9, the carrier of K9:], the carrier of K9) Element of bool [:[: the carrier of K9, the carrier of K9:], the carrier of K9:]

[: the carrier of K9, the carrier of K9:] is Relation-like non empty set

[:[: the carrier of K9, the carrier of K9:], the carrier of K9:] is Relation-like non empty set

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

the L_join of K9 . (i,a9) is Element of the carrier of K9

[i,a9] is set

the L_join of K9 . [i,a9] is set

i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

a9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

i9 is Element of K

K2 is Element of K

a . (i9,K2) is Element of K

[i9,K2] is set

a . [i9,K2] is set

i9 /\ K2 is set

a . (a9,i) is set

[a9,i] is set

a . [a9,i] is set

a9 /\ i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

i is Element of K

i9 is Element of K

a9 is Element of K

n is Relation-like Element of bool [:x,x:]

L is Relation-like Element of bool [:x,x:]

L is Relation-like Element of bool [:x,x:]

a . (i,i9) is Element of K

[i,i9] is set

a . [i,i9] is set

a . (a9,(a . (i,i9))) is Element of K

[a9,(a . (i,i9))] is set

a . [a9,(a . (i,i9))] is set

a2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

a2 /\ y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

a . (a9,(a2 /\ y9)) is set

[a9,(a2 /\ y9)] is set

a . [a9,(a2 /\ y9)] is set

K2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

K2 /\ (a2 /\ y9) is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

K2 /\ a2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

(K2 /\ a2) /\ y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

a . ((K2 /\ a2),i9) is set

[(K2 /\ a2),i9] is set

a . [(K2 /\ a2),i9] is set

a . (a9,i) is Element of K

[a9,i] is set

a . [a9,i] is set

a . ((a . (a9,i)),i9) is Element of K

[(a . (a9,i)),i9] is set

a . [(a . (a9,i)),i9] is set

a9 is Element of the carrier of K9

i is Element of the carrier of K9

i9 is Element of the carrier of K9

i "/\" i9 is Element of the carrier of K9

a9 "/\" (i "/\" i9) is Element of the carrier of K9

a9 "/\" i is Element of the carrier of K9

(a9 "/\" i) "/\" i9 is Element of the carrier of K9

the L_meet of K9 is Relation-like Function-like V18([: the carrier of K9, the carrier of K9:], the carrier of K9) Element of bool [:[: the carrier of K9, the carrier of K9:], the carrier of K9:]

[: the carrier of K9, the carrier of K9:] is Relation-like non empty set

[:[: the carrier of K9, the carrier of K9:], the carrier of K9:] is Relation-like non empty set

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

the L_meet of K9 . (a9,i) is Element of the carrier of K9

[a9,i] is set

the L_meet of K9 . [a9,i] is set

the L_meet of K9 . (a9,(i "/\" i9)) is Element of the carrier of K9

[a9,(i "/\" i9)] is set

the L_meet of K9 . [a9,(i "/\" i9)] is set

K2 is Element of K

a2 is Element of K

y9 is Element of K

a . (a2,y9) is Element of K

[a2,y9] is set

a . [a2,y9] is set

a . (K2,(a . (a2,y9))) is Element of K

[K2,(a . (a2,y9))] is set

a . [K2,(a . (a2,y9))] is set

the L_meet of K9 . (( the L_meet of K9 . (a9,i)),i9) is Element of the carrier of K9

[( the L_meet of K9 . (a9,i)),i9] is set

the L_meet of K9 . [( the L_meet of K9 . (a9,i)),i9] is set

a9 is Element of the carrier of K9

i is Element of the carrier of K9

a9 "\/" i is Element of the carrier of K9

a9 "/\" (a9 "\/" i) is Element of the carrier of K9

i9 is Element of K

K2 is Element of K

K . (i9,K2) is Element of K

[i9,K2] is set

K . [i9,K2] is set

a . (i9,(K . (i9,K2))) is Element of K

[i9,(K . (i9,K2))] is set

a . [i9,(K . (i9,K2))] is set

n is Relation-like Element of bool [:x,x:]

L is Relation-like Element of bool [:x,x:]

a2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

a2 "\/" y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

a2 /\ (a2 "\/" y9) is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

the L_meet of K9 is Relation-like Function-like V18([: the carrier of K9, the carrier of K9:], the carrier of K9) Element of bool [:[: the carrier of K9, the carrier of K9:], the carrier of K9:]

[: the carrier of K9, the carrier of K9:] is Relation-like non empty set

[:[: the carrier of K9, the carrier of K9:], the carrier of K9:] is Relation-like non empty set

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

the L_meet of K9 . (a9,(a9 "\/" i)) is Element of the carrier of K9

[a9,(a9 "\/" i)] is set

the L_meet of K9 . [a9,(a9 "\/" i)] is set

i is Element of K

a9 is Element of K

a2 is Relation-like Element of bool [:x,x:]

y9 is Relation-like Element of bool [:x,x:]

a . (a9,i) is Element of K

[a9,i] is set

a . [a9,i] is set

K2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

i9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

K2 /\ i9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

a . (i,a9) is Element of K

[i,a9] is set

a . [i,a9] is set

a9 is Element of the carrier of K9

i is Element of the carrier of K9

a9 "/\" i is Element of the carrier of K9

i "/\" a9 is Element of the carrier of K9

i9 is Element of K

K2 is Element of K

a . (i9,K2) is Element of K

[i9,K2] is set

a . [i9,K2] is set

the L_meet of K9 is Relation-like Function-like V18([: the carrier of K9, the carrier of K9:], the carrier of K9) Element of bool [:[: the carrier of K9, the carrier of K9:], the carrier of K9:]

[: the carrier of K9, the carrier of K9:] is Relation-like non empty set

[:[: the carrier of K9, the carrier of K9:], the carrier of K9:] is Relation-like non empty set

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

the L_meet of K9 . (i,a9) is Element of the carrier of K9

[i,a9] is set

the L_meet of K9 . [i,a9] is set

a9 is Element of the carrier of K9

i is Element of the carrier of K9

a9 "/\" i is Element of the carrier of K9

(a9 "/\" i) "\/" i is Element of the carrier of K9

i9 is Element of K

K2 is Element of K

a . (i9,K2) is Element of K

[i9,K2] is set

a . [i9,K2] is set

K . ((a . (i9,K2)),K2) is Element of K

[(a . (i9,K2)),K2] is set

K . [(a . (i9,K2)),K2] is set

n is Relation-like Element of bool [:x,x:]

L is Relation-like Element of bool [:x,x:]

a2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

a2 /\ y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

y9 "\/" (a2 /\ y9) is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

the L_join of K9 is Relation-like Function-like V18([: the carrier of K9, the carrier of K9:], the carrier of K9) Element of bool [:[: the carrier of K9, the carrier of K9:], the carrier of K9:]

[: the carrier of K9, the carrier of K9:] is Relation-like non empty set

[:[: the carrier of K9, the carrier of K9:], the carrier of K9:] is Relation-like non empty set

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

the L_join of K9 . ((a9 "/\" i),i) is Element of the carrier of K9

[(a9 "/\" i),i] is set

the L_join of K9 . [(a9 "/\" i),i] is set

a9 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of a9 is non empty set

the L_meet of a9 is Relation-like Function-like V18([: the carrier of a9, the carrier of a9:], the carrier of a9) Element of bool [:[: the carrier of a9, the carrier of a9:], the carrier of a9:]

[: the carrier of a9, the carrier of a9:] is Relation-like non empty set

[:[: the carrier of a9, the carrier of a9:], the carrier of a9:] is Relation-like non empty set

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

the L_join of a9 is Relation-like Function-like V18([: the carrier of a9, the carrier of a9:], the carrier of a9) Element of bool [:[: the carrier of a9, the carrier of a9:], the carrier of a9:]

i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

i9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

the L_meet of a9 . (i,i9) is set

[i,i9] is set

the L_meet of a9 . [i,i9] is set

i /\ i9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

K2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

a2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

the L_join of a9 . (K2,a2) is set

[K2,a2] is set

the L_join of a9 . [K2,a2] is set

K2 "\/" a2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

X is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of X is non empty set

the L_meet of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is Relation-like non empty set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like non empty set

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

the L_join of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

K is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of K is non empty set

the L_meet of K is Relation-like Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]

[: the carrier of K, the carrier of K:] is Relation-like non empty set

[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like non empty set

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

the L_join of K is Relation-like Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]

K is non empty set

K9 is Element of K

a is Element of K

i9 is Relation-like Element of bool [:x,x:]

K2 is Relation-like Element of bool [:x,x:]

the L_meet of X . (a,K9) is set

[a,K9] is set

the L_meet of X . [a,K9] is set

a9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

a9 /\ i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

the L_meet of K . (a,K9) is set

the L_meet of K . [a,K9] is set

K9 is Element of K

a is Element of K

i9 is Relation-like Element of bool [:x,x:]

K2 is Relation-like Element of bool [:x,x:]

the L_join of X . (a,K9) is set

[a,K9] is set

the L_join of X . [a,K9] is set

a9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

a9 "\/" i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]

the L_join of K . (a,K9) is set

the L_join of K . [a,K9] is set

x is set

X is Relation-like x -defined Function-like total set

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

K is set

K . K is set

X . K is set

[:(X . K),(X . K):] is Relation-like set

bool [:(X . K),(X . K):] is non empty set

id (X . K) is Relation-like X . K -defined X . K -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:(X . K),(X . K):]

K is Relation-like x -defined Function-like total V95() ManySortedRelation of X,X

a is set

X . a is set

[:(X . a),(X . a):] is Relation-like set

bool [:(X . a),(X . a):] is non empty set

K . a is set

K9 is Relation-like Element of bool [:(X . a),(X . a):]

id (X . a) is Relation-like X . a -defined X . a -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:(X . a),(X . a):]

x is set

x is non empty set

X is Relation-like x -defined Function-like non empty total set

K is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X

K is Relation-like x -defined Function-like non empty total set

a is set

K . a is set

X . a is set

[:(X . a),(X . a):] is Relation-like set

bool [:(X . a),(X . a):] is non empty set

K9 is Element of x

X . K9 is set

K . K9 is Relation-like Element of bool [:(X . K9),(X . K9):]

[:(X . K9),(X . K9):] is Relation-like set

bool [:(X . K9),(X . K9):] is non empty set

((X . K9),(K . K9)) is Relation-like total reflexive symmetric transitive Element of bool [:(X . K9),(X . K9):]

a is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X

K9 is set

X . K9 is set

[:(X . K9),(X . K9):] is Relation-like set

bool [:(X . K9),(X . K9):] is non empty set

a . K9 is set

a9 is Relation-like Element of bool [:(X . K9),(X . K9):]

i is Element of x

X . i is set

K . i is Relation-like Element of bool [:(X . i),(X . i):]

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

bool [:(X . i),(X . i):] is non empty set

((X . i),(K . i)) is Relation-like total reflexive symmetric transitive Element of bool [:(X . i),(X . i):]

K9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

a9 is Element of x

X . a9 is set

K9 . a9 is Relation-like Element of bool [:(X . a9),(X . a9):]

[:(X . a9),(X . a9):] is Relation-like set

bool [:(X . a9),(X . a9):] is non empty set

K . a9 is Relation-like Element of bool [:(X . a9),(X . a9):]

((X . a9),(K . a9)) is Relation-like total reflexive symmetric transitive Element of bool [:(X . a9),(X . a9):]

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

a is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K9 is set

K . K9 is set

a9 is Element of x

X . a9 is set

K . a9 is Relation-like Element of bool [:(X . a9),(X . a9):]

[:(X . a9),(X . a9):] is Relation-like set

bool [:(X . a9),(X . a9):] is non empty set

((X . a9),(K . a9)) is Relation-like total reflexive symmetric transitive Element of bool [:(X . a9),(X . a9):]

a . K9 is set

x is non empty set

X is Relation-like x -defined Function-like non empty total set

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,K) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K is Element of x

X . K is set

[:(X . K),(X . K):] is Relation-like set

bool [:(X . K),(X . K):] is non empty set

K . K is Relation-like Element of bool [:(X . K),(X . K):]

a is Relation-like total reflexive symmetric transitive Element of bool [:(X . K),(X . K):]

((X . K),a) is Relation-like total reflexive symmetric transitive Element of bool [:(X . K),(X . K):]

((X . K),(K . K)) is Relation-like total reflexive symmetric transitive Element of bool [:(X . K),(X . K):]

x is non empty set

X is Relation-like x -defined Function-like non empty total set

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K \/ K is Relation-like x -defined Function-like non empty total set

a is Relation-like x -defined Function-like non empty total set

K9 is set

a . K9 is set

X . K9 is set

[:(X . K9),(X . K9):] is Relation-like set

bool [:(X . K9),(X . K9):] is non empty set

(K \/ K) . K9 is set

a9 is Element of x

X . a9 is set

K . a9 is Relation-like Element of bool [:(X . a9),(X . a9):]

[:(X . a9),(X . a9):] is Relation-like set

bool [:(X . a9),(X . a9):] is non empty set

K . a9 is Relation-like Element of bool [:(X . a9),(X . a9):]

(K . a9) \/ (K . a9) is Relation-like Element of bool [:(X . a9),(X . a9):]

K9 is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X

(x,X,K9) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

a9 is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X

a is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,a9) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

i is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X

K9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,i) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

i is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X

K9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

a9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K9 \/ a9 is Relation-like x -defined Function-like non empty total set

a is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,i) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

a9 \/ K9 is Relation-like x -defined Function-like non empty total set

x is non empty set

X is Relation-like x -defined Function-like non empty total set

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K \/ K is Relation-like x -defined Function-like non empty total set

(x,X,K,K) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

a is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X

(x,X,a) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K9 is set

a . K9 is set

a9 is Element of x

X . a9 is set

a . a9 is Relation-like Element of bool [:(X . a9),(X . a9):]

[:(X . a9),(X . a9):] is Relation-like set

bool [:(X . a9),(X . a9):] is non empty set

((X . a9),(a . a9)) is Relation-like total reflexive symmetric transitive Element of bool [:(X . a9),(X . a9):]

(x,X,K,K) . K9 is set

x is non empty set

X is Relation-like x -defined Function-like non empty total set

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K \/ K is Relation-like x -defined Function-like non empty total set

(x,X,K,K) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

a is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X

(x,X,a) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

a9 is set

i is Element of x

K9 . i is Relation-like Element of bool [:(X . i),(X . i):]

X . i is set

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

bool [:(X . i),(X . i):] is non empty set

X . a9 is set

[:(X . a9),(X . a9):] is Relation-like set

bool [:(X . a9),(X . a9):] is non empty set

K9 . a9 is set

a . a9 is set

i9 is Relation-like total reflexive symmetric transitive Element of bool [:(X . a9),(X . a9):]

a . i is Relation-like Element of bool [:(X . i),(X . i):]

((X . i),(a . i)) is Relation-like total reflexive symmetric transitive Element of bool [:(X . i),(X . i):]

(x,X,K,K) . a9 is set

x is non empty set

X is Relation-like x -defined Function-like non empty total set

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K \/ K is Relation-like x -defined Function-like non empty total set

(x,X,K,K) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

a is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

x is non empty set

X is Relation-like x -defined Function-like non empty total set

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,K,K) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K \/ K is Relation-like x -defined Function-like non empty total set

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

x is non empty set

X is Relation-like x -defined Function-like non empty total set

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,K,K) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

a is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,(x,X,K,K),a) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,K,a) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,K,(x,X,K,a)) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K \/ a is Relation-like x -defined Function-like non empty total set

K \/ (x,X,K,a) is Relation-like x -defined Function-like non empty total set

K \/ K is Relation-like x -defined Function-like non empty total set

(x,X,K,K) \/ a is Relation-like x -defined Function-like non empty total set

K9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K \/ K is Relation-like x -defined Function-like non empty total set

(x,X,K,K) \/ a is Relation-like x -defined Function-like non empty total set

K \/ a is Relation-like x -defined Function-like non empty total set

K \/ (x,X,K,a) is Relation-like x -defined Function-like non empty total set

x is non empty set

X is Relation-like x -defined Function-like non empty total set

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,K,K) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K /\ (x,X,K,K) is Relation-like x -defined Function-like non empty total set

K \/ K is Relation-like x -defined Function-like non empty total set

x is non empty set

X is Relation-like x -defined Function-like non empty total set

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K /\ K is Relation-like x -defined Function-like non empty total set

K \/ (K /\ K) is Relation-like x -defined Function-like non empty total set

a is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

a is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,K,a) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

x is non empty set

X is Relation-like x -defined Function-like non empty total set

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K /\ K is Relation-like x -defined Function-like non empty total set

a is set

(K /\ K) . a is set

X . a is set

[:(X . a),(X . a):] is Relation-like set

bool [:(X . a),(X . a):] is non empty set

K . a is set

K . a is set

K9 is Relation-like Element of bool [:(X . a),(X . a):]

a9 is Relation-like Element of bool [:(X . a),(X . a):]

K9 /\ a9 is Relation-like Element of bool [:(X . a),(X . a):]

a is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X

K9 is set

X . K9 is set

[:(X . K9),(X . K9):] is Relation-like set

bool [:(X . K9),(X . K9):] is non empty set

a . K9 is set

a9 is Relation-like Element of bool [:(X . K9),(X . K9):]

K . K9 is set

i is Relation-like Element of bool [:(X . K9),(X . K9):]

K . K9 is set

K2 is Relation-like Element of bool [:(X . K9),(X . K9):]

a2 is Relation-like total reflexive symmetric transitive Element of bool [:(X . K9),(X . K9):]

i9 is Relation-like total reflexive symmetric transitive Element of bool [:(X . K9),(X . K9):]

a2 /\ i9 is Relation-like total reflexive symmetric transitive Element of bool [:(X . K9),(X . K9):]

x is non empty set

X is Relation-like x -defined Function-like non empty total set

the Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K is Relation-like x -defined Function-like non empty total set

product K is set

a is set

K9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

dom K is non empty Element of bool x

bool x is non empty set

a9 is set

K9 . a9 is set

K . a9 is set

i is Element of x

K9 . i is Relation-like Element of bool [:(X . i),(X . i):]

X . i is set

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

bool [:(X . i),(X . i):] is non empty set

K . i is set

dom K9 is non empty Element of bool x

K9 is non empty set

a9 is Element of K9

i is Element of K9

i9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K2 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,i9,K2) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

y9 is Element of K9

n is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

n \/ L is Relation-like x -defined Function-like non empty total set

[:K9,K9:] is Relation-like non empty set

[:[:K9,K9:],K9:] is Relation-like non empty set

bool [:[:K9,K9:],K9:] is non empty set

a9 is Relation-like Function-like V18([:K9,K9:],K9) Element of bool [:[:K9,K9:],K9:]

i is Element of K9

i9 is Element of K9

K2 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

a2 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K2 /\ a2 is Relation-like x -defined Function-like non empty total set

n is set

(K2 /\ a2) . n is set

X . n is set

[:(X . n),(X . n):] is Relation-like set

bool [:(X . n),(X . n):] is non empty set

L is Element of x

X . L is set

K2 . L is Relation-like Element of bool [:(X . L),(X . L):]

[:(X . L),(X . L):] is Relation-like set

bool [:(X . L),(X . L):] is non empty set

a2 . L is Relation-like Element of bool [:(X . L),(X . L):]

(K2 . L) /\ (a2 . L) is Relation-like Element of bool [:(X . L),(X . L):]

n is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X

L is set

X . L is set

[:(X . L),(X . L):] is Relation-like set

bool [:(X . L),(X . L):] is non empty set

n . L is set

L is Relation-like Element of bool [:(X . L),(X . L):]

L is Element of x

K2 . L is Relation-like Element of bool [:(X . L),(X . L):]

X . L is set

[:(X . L),(X . L):] is Relation-like set

bool [:(X . L),(X . L):] is non empty set

a2 . L is Relation-like Element of bool [:(X . L),(X . L):]

c

b9 is Relation-like Element of bool [:(X . L),(X . L):]

EQR is Relation-like total reflexive symmetric transitive Element of bool [:(X . L),(X . L):]

c9 is Relation-like total reflexive symmetric transitive Element of bool [:(X . L),(X . L):]

EQR /\ c9 is Relation-like total reflexive symmetric transitive Element of bool [:(X . L),(X . L):]

L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

L is Element of K9

L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

c

L /\ c

i is Relation-like Function-like V18([:K9,K9:],K9) Element of bool [:[:K9,K9:],K9:]

LattStr(# K9,a9,i #) is non empty strict LattStr

a2 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K2 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K2 \/ a2 is Relation-like x -defined Function-like non empty total set

y9 is Element of K9

n is Element of K9

a9 . (y9,n) is Element of K9

[y9,n] is set

a9 . [y9,n] is set

a9 . (K2,a2) is set

[K2,a2] is set

a9 . [K2,a2] is set

(x,X,K2,a2) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

L is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X

(x,X,L) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K2 is Element of K9

a2 is Element of K9

y9 is Element of K9

a9 . (a2,y9) is Element of K9

[a2,y9] is set

a9 . [a2,y9] is set

a9 . (K2,(a9 . (a2,y9))) is Element of K9

[K2,(a9 . (a2,y9))] is set

a9 . [K2,(a9 . (a2,y9))] is set

L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,L,L) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

a9 . (K2,(x,X,L,L)) is set

[K2,(x,X,L,L)] is set

a9 . [K2,(x,X,L,L)] is set

n is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,n,(x,X,L,L)) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,n,L) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,(x,X,n,L),L) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

a9 . ((x,X,n,L),y9) is set

[(x,X,n,L),y9] is set

a9 . [(x,X,n,L),y9] is set

a9 . (K2,a2) is Element of K9

[K2,a2] is set

a9 . [K2,a2] is set

a9 . ((a9 . (K2,a2)),y9) is Element of K9

[(a9 . (K2,a2)),y9] is set

a9 . [(a9 . (K2,a2)),y9] is set

i9 is non empty LattStr

the carrier of i9 is non empty set

K2 is Element of the carrier of i9

a2 is Element of the carrier of i9

y9 is Element of the carrier of i9

a2 "\/" y9 is Element of the carrier of i9

K2 "\/" (a2 "\/" y9) is Element of the carrier of i9

K2 "\/" a2 is Element of the carrier of i9

(K2 "\/" a2) "\/" y9 is Element of the carrier of i9

the L_join of i9 is Relation-like Function-like V18([: the carrier of i9, the carrier of i9:], the carrier of i9) Element of bool [:[: the carrier of i9, the carrier of i9:], the carrier of i9:]

[: the carrier of i9, the carrier of i9:] is Relation-like non empty set

[:[: the carrier of i9, the carrier of i9:], the carrier of i9:] is Relation-like non empty set

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

the L_join of i9 . (K2,a2) is Element of the carrier of i9

[K2,a2] is set

the L_join of i9 . [K2,a2] is set

the L_join of i9 . (K2,(a2 "\/" y9)) is Element of the carrier of i9

[K2,(a2 "\/" y9)] is set

the L_join of i9 . [K2,(a2 "\/" y9)] is set

n is Element of K9

L is Element of K9

L is Element of K9

a9 . (L,L) is Element of K9

[L,L] is set

a9 . [L,L] is set

a9 . (n,(a9 . (L,L))) is Element of K9

[n,(a9 . (L,L))] is set

a9 . [n,(a9 . (L,L))] is set

the L_join of i9 . (( the L_join of i9 . (K2,a2)),y9) is Element of the carrier of i9

[( the L_join of i9 . (K2,a2)),y9] is set

the L_join of i9 . [( the L_join of i9 . (K2,a2)),y9] is set

a2 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K2 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

n is Element of K9

y9 is Element of K9

i . (K2,a2) is set

[K2,a2] is set

i . [K2,a2] is set

K2 /\ a2 is Relation-like x -defined Function-like non empty total set

K2 is Element of K9

a2 is Element of K9

y9 is Element of K9

L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

L /\ L is Relation-like x -defined Function-like non empty total set

n is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

n /\ L is Relation-like x -defined Function-like non empty total set

i . (a2,y9) is Element of K9

[a2,y9] is set

i . [a2,y9] is set

i . (K2,(i . (a2,y9))) is Element of K9

[K2,(i . (a2,y9))] is set

i . [K2,(i . (a2,y9))] is set

L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

i . (K2,L) is set

[K2,L] is set

i . [K2,L] is set

n /\ (L /\ L) is Relation-like x -defined Function-like non empty total set

(n /\ L) /\ L is Relation-like x -defined Function-like non empty total set

c

i . (c

[c

i . [c

i . (K2,a2) is Element of K9

[K2,a2] is set

i . [K2,a2] is set

i . ((i . (K2,a2)),y9) is Element of K9

[(i . (K2,a2)),y9] is set

i . [(i . (K2,a2)),y9] is set

K2 is Element of the carrier of i9

a2 is Element of the carrier of i9

y9 is Element of the carrier of i9

a2 "/\" y9 is Element of the carrier of i9

K2 "/\" (a2 "/\" y9) is Element of the carrier of i9

K2 "/\" a2 is Element of the carrier of i9

(K2 "/\" a2) "/\" y9 is Element of the carrier of i9

the L_meet of i9 is Relation-like Function-like V18([: the carrier of i9, the carrier of i9:], the carrier of i9) Element of bool [:[: the carrier of i9, the carrier of i9:], the carrier of i9:]

[: the carrier of i9, the carrier of i9:] is Relation-like non empty set

[:[: the carrier of i9, the carrier of i9:], the carrier of i9:] is Relation-like non empty set

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

the L_meet of i9 . (K2,a2) is Element of the carrier of i9

[K2,a2] is set

the L_meet of i9 . [K2,a2] is set

the L_meet of i9 . (K2,(a2 "/\" y9)) is Element of the carrier of i9

[K2,(a2 "/\" y9)] is set

the L_meet of i9 . [K2,(a2 "/\" y9)] is set

n is Element of K9

L is Element of K9

L is Element of K9

i . (L,L) is Element of K9

[L,L] is set

i . [L,L] is set

i . (n,(i . (L,L))) is Element of K9

[n,(i . (L,L))] is set

i . [n,(i . (L,L))] is set

the L_meet of i9 . (( the L_meet of i9 . (K2,a2)),y9) is Element of the carrier of i9

[( the L_meet of i9 . (K2,a2)),y9] is set

the L_meet of i9 . [( the L_meet of i9 . (K2,a2)),y9] is set

K2 is Element of K9

a2 is Element of K9

a9 . (K2,a2) is Element of K9

[K2,a2] is set

a9 . [K2,a2] is set

y9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

n is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,y9,n) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

a9 . (a2,K2) is Element of K9

[a2,K2] is set

a9 . [a2,K2] is set

K2 is Element of the carrier of i9

a2 is Element of the carrier of i9

K2 "\/" a2 is Element of the carrier of i9

a2 "\/" K2 is Element of the carrier of i9

y9 is Element of K9

n is Element of K9

a9 . (y9,n) is Element of K9

[y9,n] is set

a9 . [y9,n] is set

the L_join of i9 is Relation-like Function-like V18([: the carrier of i9, the carrier of i9:], the carrier of i9) Element of bool [:[: the carrier of i9, the carrier of i9:], the carrier of i9:]

[: the carrier of i9, the carrier of i9:] is Relation-like non empty set

[:[: the carrier of i9, the carrier of i9:], the carrier of i9:] is Relation-like non empty set

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

the L_join of i9 . (a2,K2) is Element of the carrier of i9

[a2,K2] is set

the L_join of i9 . [a2,K2] is set

K2 is Element of the carrier of i9

a2 is Element of the carrier of i9

K2 "/\" a2 is Element of the carrier of i9

(K2 "/\" a2) "\/" a2 is Element of the carrier of i9

y9 is Element of K9

n is Element of K9

i . (y9,n) is Element of K9

[y9,n] is set

i . [y9,n] is set

a9 . ((i . (y9,n)),n) is Element of K9

[(i . (y9,n)),n] is set

a9 . [(i . (y9,n)),n] is set

L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

L /\ L is Relation-like x -defined Function-like non empty total set

L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,L,L) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

the L_join of i9 is Relation-like Function-like V18([: the carrier of i9, the carrier of i9:], the carrier of i9) Element of bool [:[: the carrier of i9, the carrier of i9:], the carrier of i9:]

[: the carrier of i9, the carrier of i9:] is Relation-like non empty set

[:[: the carrier of i9, the carrier of i9:], the carrier of i9:] is Relation-like non empty set

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

the L_join of i9 . ((K2 "/\" a2),a2) is Element of the carrier of i9

[(K2 "/\" a2),a2] is set

the L_join of i9 . [(K2 "/\" a2),a2] is set

K2 is Element of K9

a2 is Element of K9

i . (K2,a2) is Element of K9

[K2,a2] is set

i . [K2,a2] is set

n is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

y9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

n /\ y9 is Relation-like x -defined Function-like non empty total set

i . (a2,K2) is Element of K9

[a2,K2] is set

i . [a2,K2] is set

K2 is Element of the carrier of i9

a2 is Element of the carrier of i9

K2 "/\" a2 is Element of the carrier of i9

a2 "/\" K2 is Element of the carrier of i9

y9 is Element of K9

n is Element of K9

i . (y9,n) is Element of K9

[y9,n] is set

i . [y9,n] is set

the L_meet of i9 is Relation-like Function-like V18([: the carrier of i9, the carrier of i9:], the carrier of i9) Element of bool [:[: the carrier of i9, the carrier of i9:], the carrier of i9:]

[: the carrier of i9, the carrier of i9:] is Relation-like non empty set

[:[: the carrier of i9, the carrier of i9:], the carrier of i9:] is Relation-like non empty set

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

the L_meet of i9 . (a2,K2) is Element of the carrier of i9

[a2,K2] is set

the L_meet of i9 . [a2,K2] is set

K2 is Element of the carrier of i9

a2 is Element of the carrier of i9

K2 "\/" a2 is Element of the carrier of i9

K2 "/\" (K2 "\/" a2) is Element of the carrier of i9

y9 is Element of K9

n is Element of K9

a9 . (y9,n) is Element of K9

[y9,n] is set

a9 . [y9,n] is set

i . (y9,(a9 . (y9,n))) is Element of K9

[y9,(a9 . (y9,n))] is set

i . [y9,(a9 . (y9,n))] is set

L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

(x,X,L,L) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

L /\ (x,X,L,L) is Relation-like x -defined Function-like non empty total set

the L_meet of i9 is Relation-like Function-like V18([: the carrier of i9, the carrier of i9:], the carrier of i9) Element of bool [:[: the carrier of i9, the carrier of i9:], the carrier of i9:]

[: the carrier of i9, the carrier of i9:] is Relation-like non empty set

[:[: the carrier of i9, the carrier of i9:], the carrier of i9:] is Relation-like non empty set

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

the L_meet of i9 . (K2,(K2 "\/" a2)) is Element of the carrier of i9

[K2,(K2 "\/" a2)] is set

the L_meet of i9 . [K2,(K2 "\/" a2)] is set

K2 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of K2 is non empty set

the L_meet of K2 is Relation-like Function-like V18([: the carrier of K2, the carrier of K2:], the carrier of K2) Element of bool [:[: the carrier of K2, the carrier of K2:], the carrier of K2:]

[: the carrier of K2, the carrier of K2:] is Relation-like non empty set

[:[: the carrier of K2, the carrier of K2:], the carrier of K2:] is Relation-like non empty set

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

the L_join of K2 is Relation-like Function-like V18([: the carrier of K2, the carrier of K2:], the carrier of K2) Element of bool [:[: the carrier of K2, the carrier of K2:], the carrier of K2:]

a2 is set

a2 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

y9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

the L_meet of K2 . (a2,y9) is set

[a2,y9] is set

the L_meet of K2 . [a2,y9] is set

a2 /\ y9 is Relation-like x -defined Function-like non empty total set

n is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

the L_join of K2 . (n,L) is set

[n,L] is set

the L_join of K2 . [n,L] is set

(x,X,n,L) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

K is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of K is non empty set

the L_meet of K is Relation-like Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]

[: the carrier of K, the carrier of K:] is Relation-like non empty set

[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like non empty set

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

the L_join of K is Relation-like Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]

K is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of K is non empty set

the L_meet of K is Relation-like Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]

[: the carrier of K, the carrier of K:] is Relation-like non empty set

[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like non empty set

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

the L_join of K is Relation-like Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]

K9 is set

a is non empty set

K9 is Element of a

a9 is Element of a

the L_meet of K . (K9,a9) is set

[K9,a9] is set

the L_meet of K . [K9,a9] is set

i is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

i9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

i /\ i9 is Relation-like x -defined Function-like non empty total set

the L_meet of K . (K9,a9) is set

the L_meet of K . [K9,a9] is set

the L_join of K . (K9,a9) is set

the L_join of K . [K9,a9] is set

(x,X,i,i9) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X

the L_join of K . (K9,a9) is set

the L_join of K . [K9,a9] is set

x is non empty V71() ManySortedSign

the carrier of x is non empty set

X is MSAlgebra over x

the Sorts of X is Relation-like the carrier of x -defined Function-like non empty total set

K is Relation-like the carrier of x -defined Function-like non empty total V95() ManySortedRelation of the Sorts of X, the Sorts of X

x is non empty non void V71() ManySortedSign

the carrier' of x is non empty set

the carrier of x is non empty set

X is non-empty MSAlgebra over x

the Sorts of X is Relation-like non-empty non empty-yielding the carrier of x -defined Function-like non empty total set

K is Element of the carrier' of x

the_arity_of K is Relation-like NAT -defined the carrier of x -valued Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of x *

the carrier of x * is functional non empty FinSequence-membered M15( the carrier of x)

Args (K,X) is functional non empty Element of rng ( the Sorts of X #)

the Sorts of X # is Relation-like the carrier of x * -defined Function-like non empty total set

rng ( the Sorts of X #) is non empty set

Result (K,X) is non empty Element of rng the Sorts of X

rng the Sorts of X is non empty V38() set

Den (K,X) is Relation-like Function-like V18( Args (K,X), Result (K,X)) Element of bool [:(Args (K,X)),(Result (K,X)):]

[:(Args (K,X)),(Result (K,X)):] is Relation-like non empty set

bool [:(Args (K,X)),(Result (K,X)):] is non empty set

the_result_sort_of K is Element of the carrier of x

the Sorts of X . (the_result_sort_of K) is non empty set

K is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of X, the Sorts of X

a is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of X, the Sorts of X

K . (the_result_sort_of K) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . (the_result_sort_of K)),( the Sorts of X . (the_result_sort_of K)):]

[:( the Sorts of X . (the_result_sort_of K)),( the Sorts of X . (the_result_sort_of K)):] is Relation-like non empty set

bool [:( the Sorts of X . (the_result_sort_of K)),( the Sorts of X . (the_result_sort_of K)):] is non empty set

a . (the_result_sort_of K) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . (the_result_sort_of K)),( the Sorts of X . (the_result_sort_of K)):]

(K . (the_result_sort_of K)) \/ (a . (the_result_sort_of K)) is Relation-like reflexive symmetric Element of bool [:( the Sorts of X . (the_result_sort_of K)),( the Sorts of X . (the_result_sort_of K)):]

K9 is set

a9 is set

[K9,a9] is set

<*K9*> is Relation-like NAT -defined Function-like constant non empty trivial V50() V57(1) FinSequence-like FinSubsequence-like set

<*a9*> is Relation-like NAT -defined Function-like constant non empty trivial V50() V57(1) FinSequence-like FinSubsequence-like set

i is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set

len i is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT

(len i) + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT

(the_arity_of K) /. ((len i) + 1) is Element of the carrier of x

the Sorts of X . ((the_arity_of K) /. ((len i) + 1)) is non empty set

K . ((the_arity_of K) /. ((len i) + 1)) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))),( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))):]

[:( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))),( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))):] is Relation-like non empty set

bool [:( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))),( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))):] is non empty set

a . ((the_arity_of K) /. ((len i) + 1)) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))),( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))):]

(K . ((the_arity_of K) /. ((len i) + 1))) \/ (a . ((the_arity_of K) /. ((len i) + 1))) is Relation-like reflexive symmetric Element of bool [:( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))),( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))):]

i ^ <*K9*> is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set

i9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set

(i ^ <*K9*>) ^ i9 is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set

i ^ <*a9*> is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set

(i ^ <*a9*>) ^ i9 is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set

K2 is Relation-like Function-like Element of Args (K,X)

a2 is Relation-like Function-like Element of Args (K,X)

(Den (K,X)) . K2 is Element of Result (K,X)

(Den (K,X)) . a2 is Element of Result (K,X)

[((Den (K,X)) . K2),((Den (K,X)) . a2)] is set

<*a9*> ^ i9 is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set

i ^ (<*a9*> ^ i9) is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set

<*K9*> ^ i9 is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set

i ^ (<*K9*> ^ i9) is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set

dom K2 is set

y9 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set

K2 . y9 is set

a2 . y9 is set

[(K2 . y9),(a2 . y9)] is set

(the_arity_of K) /. y9 is Element of the carrier of x

K . ((the_arity_of K) /. y9) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of K) /. y9)),( the Sorts of X . ((the_arity_of K) /. y9)):]

the Sorts of X . ((the_arity_of K) /. y9) is non empty set

[:( the Sorts of X . ((the_arity_of K) /. y9)),( the Sorts of X . ((the_arity_of K) /. y9)):] is Relation-like non empty set

bool [:( the Sorts of X . ((the_arity_of K) /. y9)),( the Sorts of X . ((the_arity_of K) /. y9)):] is non empty set

dom (the_arity_of K) is Element of bool NAT

(the_arity_of K) * the Sorts of X is Relation-like non-empty NAT -defined dom (the_arity_of K) -defined Function-like total set

dom ((the_arity_of K) * the Sorts of X) is Element of bool NAT

n is non empty set

L is Relation-like non-empty non empty-yielding n -defined Function-like non empty total set

product L is non empty set

pi ((Args (K,X)),y9) is set

the Arity of x is Relation-like Function-like V18( the carrier' of x, the carrier of x * ) Element of bool [: the carrier' of x,( the carrier of x *):]

[: the carrier' of x,( the carrier of x *):] is Relation-like non empty set

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

the Arity of x * ( the Sorts of X #) is Relation-like Function-like set

( the Arity of x * ( the Sorts of X #)) . K is set

pi ((( the Arity of x * ( the Sorts of X #)) . K),y9) is set

the Arity of x . K is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of x *

( the Sorts of X #) . ( the Arity of x . K) is set

pi ((( the Sorts of X #) . ( the Arity of x . K)),y9) is set

( the Sorts of X #) . (the_arity_of K) is set

pi ((( the Sorts of X #) . (the_arity_of K)),y9) is set

product ((the_arity_of K) * the Sorts of X) is set

pi ((product ((the_arity_of K) * the Sorts of X)),y9) is set

((the_arity_of K) * the Sorts of X) . y9 is set

(the_arity_of K) . y9 is set

the Sorts of X . ((the_arity_of K) . y9) is set

dom (i ^ <*K9*>) is non empty Element of bool NAT

dom i9 is Element of bool NAT

len (i ^ <*K9