:: 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

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

bool is non empty V50() set

the carrier of Nat_Lattice is non empty set
bool NAT is non empty V50() set
NATPLUS is non empty Element of bool NAT

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

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:]

x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set

(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 set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
{ b1 where b1 is Relation-like Element of bool [:x,x:] : b1 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:] } is set

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:]

i9 is Element of K
K2 is Element of K
y9 is Relation-like 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:]

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

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

L is Element of K
K . (a9,i) is set
[a9,i] is set
K . [a9,i] is set

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

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

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

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

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

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

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

K2 /\ (a2 /\ y9) 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 /\ (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

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:]

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

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:]

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

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

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:]

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

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

the L_join of K . (a,K9) is set
the L_join of K . [a,K9] is set
x is 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

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):]

x is set
x is non empty 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):]

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):]

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):]

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

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

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):]

x is non empty set

(x,X,K,K) 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,X,K,K) 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,X,K,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,X,K,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,X,K,K) 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

K \/ (x,X,K,a) 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

(x,X,K,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,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

x is non empty set

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

(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

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):]

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

product K is set
a is set

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

(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

[: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

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):]

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):]
c17 is Relation-like Element of bool [:(X . L),(X . L):]
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 Element of K9

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

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

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

(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

(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

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 is Element of K9
a2 is Element of K9
y9 is Element of K9

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

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

i . (c17,y9) is set
[c17,y9] is set
i . [c17,y9] is set
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

(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

(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

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

(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

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

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

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

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:]

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

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

K is 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 . is non empty set

K . is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ),( the Sorts of X . ):]
[:( the Sorts of X . ),( the Sorts of X . ):] is Relation-like non empty set
bool [:( the Sorts of X . ),( the Sorts of X . ):] is non empty set
a . is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ),( the Sorts of X . ):]
(K . ) \/ (a . ) is Relation-like reflexive symmetric Element of bool [:( the Sorts of X . ),( the Sorts of X . ):]
K9 is set
a9 is set
[K9,a9] is 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
() /. ((len i) + 1) is Element of the carrier of x
the Sorts of X . (() /. ((len i) + 1)) is non empty set
K . (() /. ((len i) + 1)) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . (() /. ((len i) + 1))),( the Sorts of X . (() /. ((len i) + 1))):]
[:( the Sorts of X . (() /. ((len i) + 1))),( the Sorts of X . (() /. ((len i) + 1))):] is Relation-like non empty set
bool [:( the Sorts of X . (() /. ((len i) + 1))),( the Sorts of X . (() /. ((len i) + 1))):] is non empty set
a . (() /. ((len i) + 1)) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . (() /. ((len i) + 1))),( the Sorts of X . (() /. ((len i) + 1))):]
(K . (() /. ((len i) + 1))) \/ (a . (() /. ((len i) + 1))) is Relation-like reflexive symmetric Element of bool [:( the Sorts of X . (() /. ((len i) + 1))),( the Sorts of X . (() /. ((len i) + 1))):]

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

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
() /. y9 is Element of the carrier of x
K . (() /. y9) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . (() /. y9)),( the Sorts of X . (() /. y9)):]
the Sorts of X . (() /. y9) is non empty set
[:( the Sorts of X . (() /. y9)),( the Sorts of X . (() /. y9)):] is Relation-like non empty set
bool [:( the Sorts of X . (() /. y9)),( the Sorts of X . (() /. y9)):] is non empty set
dom () is Element of bool NAT

dom (() * the Sorts of X) is Element of bool NAT
n is non empty 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 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 #) . () is set
pi ((( the Sorts of X #) . ()),y9) is set
product (() * the Sorts of X) is set
pi ((product (() * the Sorts of X)),y9) is set
(() * the Sorts of X) . y9 is set
() . y9 is set
the Sorts of X . (() . y9) is set
dom (i ^ <*K9*>) is non empty Element of bool NAT
dom i9 is Element of bool NAT
len (i ^ <*K9