K152() is Element of K10(K148())
K148() is set
K10(K148()) is non empty set
K98() is set
K10(K98()) is non empty set
K10(K152()) is non empty set
{} is empty Relation-like non-empty empty-yielding K152() -defined Function-like one-to-one constant functional V31() V79() V80() V81() set
1 is non empty set
{{},1} is non empty set
2 is non empty set
3 is non empty set
S1 is non empty V99() V100() V101() RelStr
the carrier of S1 is non empty set
U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
U0 /\ B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
L is Element of the carrier of S1
G1 is Element of the carrier of S1
B . L is set
B . G1 is set
U0 . L is set
U0 . G1 is set
B . L is set
B . G1 is set
(U0 /\ B) . L is set
(U0 . L) /\ (B . L) is set
(U0 /\ B) . G1 is set
(U0 . G1) /\ (B . G1) is set
S1 is non empty V99() V100() V101() RelStr
the carrier of S1 is non empty set
U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
U0 \/ B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
L is Element of the carrier of S1
G1 is Element of the carrier of S1
B . L is set
B . G1 is set
U0 . L is set
U0 . G1 is set
B . L is set
B . G1 is set
(U0 \/ B) . L is set
(U0 . L) \/ (B . L) is set
(U0 \/ B) . G1 is set
(U0 . G1) \/ (B . G1) is set
S1 is non empty V99() V100() V101() RelStr
the carrier of S1 is non empty set
U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of U0
S1 is non empty V99() V100() V101() RelStr
the carrier of S1 is non empty set
U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of U0
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
{{}} is non empty functional set
the Relation-like Function-like Element of {{}} is Relation-like Function-like Element of {{}}
TrivialOSA (S1,{{}}, the Relation-like Function-like Element of {{}}) is strict non-empty order-sorted monotone MSAlgebra over S1
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is non-empty order-sorted MSAlgebra over S1
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
S1 is non empty non void V52() strict all-with_const_op ManySortedSign
OSSign S1 is non empty non void V52() V99() V100() V101() V148() strict order-sorted discernable op-discrete monotone V170() OverloadedRSSign
the carrier of (OSSign S1) is non empty set
U0 is Element of the carrier of (OSSign S1)
the carrier of S1 is non empty set
B is Element of the carrier of S1
the carrier' of S1 is non empty set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))
the carrier of S1 * is non empty functional V81() M12( the carrier of S1)
K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set
K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))
K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set
K10(K11( the carrier' of S1, the carrier of S1)) is non empty set
B is Element of the carrier' of S1
the Arity of S1 . B is Relation-like K152() -defined Function-like V31() V79() V80() set
the ResultSort of S1 . B is set
the carrier' of (OSSign S1) is non empty set
the Arity of (OSSign S1) is Relation-like the carrier' of (OSSign S1) -defined the carrier of (OSSign S1) * -valued Function-like V21( the carrier' of (OSSign S1), the carrier of (OSSign S1) * ) Element of K10(K11( the carrier' of (OSSign S1),( the carrier of (OSSign S1) *)))
the carrier of (OSSign S1) * is non empty functional V81() M12( the carrier of (OSSign S1))
K11( the carrier' of (OSSign S1),( the carrier of (OSSign S1) *)) is non empty Relation-like set
K10(K11( the carrier' of (OSSign S1),( the carrier of (OSSign S1) *))) is non empty set
the Arity of (OSSign S1) . B is Relation-like K152() -defined Function-like V31() V79() V80() set
the ResultSort of (OSSign S1) is Relation-like the carrier' of (OSSign S1) -defined the carrier of (OSSign S1) -valued Function-like V21( the carrier' of (OSSign S1), the carrier of (OSSign S1)) Element of K10(K11( the carrier' of (OSSign S1), the carrier of (OSSign S1)))
K11( the carrier' of (OSSign S1), the carrier of (OSSign S1)) is non empty Relation-like set
K10(K11( the carrier' of (OSSign S1), the carrier of (OSSign S1))) is non empty set
the ResultSort of (OSSign S1) . B is set
the non empty non void V52() strict all-with_const_op ManySortedSign is non empty non void V52() strict all-with_const_op ManySortedSign
OSSign the non empty non void V52() strict all-with_const_op ManySortedSign is non empty non void V52() V99() V100() V101() V148() strict order-sorted discernable op-discrete monotone V170() OverloadedRSSign
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is order-sorted MSAlgebra over S1
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the carrier of S1 is non empty set
the Charact of U0 is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * ( the Sorts of U0 #), the ResultSort of S1 * the Sorts of U0
the carrier' of S1 is non empty set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))
the carrier of S1 * is non empty functional V81() M12( the carrier of S1)
K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set
K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set
the Sorts of U0 # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))
K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set
K10(K11( the carrier' of S1, the carrier of S1)) is non empty set
the ResultSort of S1 * the Sorts of U0 is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict MSAlgebra over S1
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is order-sorted MSAlgebra over S1
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the carrier of S1 is non empty set
the Charact of U0 is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * ( the Sorts of U0 #), the ResultSort of S1 * the Sorts of U0
the carrier' of S1 is non empty set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))
the carrier of S1 * is non empty functional V81() M12( the carrier of S1)
K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set
K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set
the Sorts of U0 # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))
K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set
K10(K11( the carrier' of S1, the carrier of S1)) is non empty set
the ResultSort of S1 * the Sorts of U0 is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict MSAlgebra over S1
B is strict MSSubAlgebra of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is order-sorted MSAlgebra over S1
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the carrier of S1 is non empty set
the Charact of U0 is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * ( the Sorts of U0 #), the ResultSort of S1 * the Sorts of U0
the carrier' of S1 is non empty set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))
the carrier of S1 * is non empty functional V81() M12( the carrier of S1)
K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set
K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set
the Sorts of U0 # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))
K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set
K10(K11( the carrier' of S1, the carrier of S1)) is non empty set
the ResultSort of S1 * the Sorts of U0 is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict MSAlgebra over S1
B is order-sorted MSSubAlgebra of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is non-empty order-sorted MSAlgebra over S1
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set
the carrier of S1 is non empty set
the Charact of U0 is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * ( the Sorts of U0 #), the ResultSort of S1 * the Sorts of U0
the carrier' of S1 is non empty set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))
the carrier of S1 * is non empty functional V81() M12( the carrier of S1)
K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set
K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set
the Sorts of U0 # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))
K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set
K10(K11( the carrier' of S1, the carrier of S1)) is non empty set
the ResultSort of S1 * the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict non-empty MSAlgebra over S1
B is strict order-sorted MSSubAlgebra of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
the carrier' of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
B is MSAlgebra over S1
the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Charact of B is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * ( the Sorts of B #), the ResultSort of S1 * the Sorts of B
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))
the carrier of S1 * is non empty functional V81() M12( the carrier of S1)
K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set
K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set
the Sorts of B # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * ( the Sorts of B #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))
K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set
K10(K11( the carrier' of S1, the carrier of S1)) is non empty set
the ResultSort of S1 * the Sorts of B is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
Opers (U0,B) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * (B #), the ResultSort of S1 * B
B # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * (B #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
the ResultSort of S1 * B is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
Opers (U0,B) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * (B #), the ResultSort of S1 * B
B # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * (B #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
the ResultSort of S1 * B is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
B is Element of the carrier of S1
{ (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= B } is set
union { (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= B } is set
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of U0 . B is set
K10(( the Sorts of U0 . B)) is non empty set
L is set
G1 is Element of the carrier of S1
Constants (U0,G1) is Element of K10(( the Sorts of U0 . G1))
the Sorts of U0 . G1 is set
K10(( the Sorts of U0 . G1)) is non empty set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
B is Element of the carrier of S1
Constants (U0,B) is Element of K10(( the Sorts of U0 . B))
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of U0 . B is set
K10(( the Sorts of U0 . B)) is non empty set
(S1,U0,B) is Element of K10(( the Sorts of U0 . B))
{ (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= B } is set
union { (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= B } is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
{ (U0 . b1) where b1 is Element of the carrier of S1 : b1 <= a1 } is set
union { (U0 . b1) where b1 is Element of the carrier of S1 : b1 <= a1 } is set
B is Relation-like Function-like set
dom B is set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
G1 is Element of the carrier of S1
a is Element of the carrier of S1
L . G1 is set
L . a is set
a1 is set
{ (U0 . b1) where b1 is Element of the carrier of S1 : b1 <= G1 } is set
union { (U0 . b1) where b1 is Element of the carrier of S1 : b1 <= G1 } is set
a2 is set
a2 is Element of the carrier of S1
U0 . a2 is set
{ (U0 . b1) where b1 is Element of the carrier of S1 : b1 <= a } is set
union { (U0 . b1) where b1 is Element of the carrier of S1 : b1 <= a } is set
G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
a is Element of the carrier of S1
G1 . a is set
{ (U0 . b1) where b1 is Element of the carrier of S1 : b1 <= a } is set
union { (U0 . b1) where b1 is Element of the carrier of S1 : b1 <= a } is set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
L is set
B . L is set
B . L is set
G1 is Element of the carrier of S1
{ (U0 . b1) where b1 is Element of the carrier of S1 : b1 <= G1 } is set
union { (U0 . b1) where b1 is Element of the carrier of S1 : b1 <= G1 } is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
B is set
U0 . B is set
(S1,U0) . B is set
B is Element of the carrier of S1
U0 . B is set
{ (U0 . b1) where b1 is Element of the carrier of S1 : b1 <= B } is set
union { (U0 . b1) where b1 is Element of the carrier of S1 : b1 <= B } is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
B is set
(S1,U0) . B is set
B . B is set
G1 is set
L is Element of the carrier of S1
(S1,U0) . L is set
{ (U0 . b1) where b1 is Element of the carrier of S1 : b1 <= L } is set
union { (U0 . b1) where b1 is Element of the carrier of S1 : b1 <= L } is set
a is set
a1 is Element of the carrier of S1
U0 . a1 is set
B . a1 is set
B . L is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
{ (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= a1 } is set
union { (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= a1 } is set
B is Relation-like Function-like set
dom B is set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
L is set
B . L is set
the Sorts of U0 . L is set
G1 is Element of the carrier of S1
B . G1 is set
(S1,U0,G1) is Element of K10(( the Sorts of U0 . G1))
the Sorts of U0 . G1 is set
K10(( the Sorts of U0 . G1)) is non empty set
{ (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= G1 } is set
union { (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= G1 } is set
L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
a is Element of the carrier of S1
a1 is Element of the carrier of S1
G1 . a is set
G1 . a1 is set
a2 is set
{ (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= a } is set
union { (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= a } is set
a2 is set
C1 is Element of the carrier of S1
Constants (U0,C1) is Element of K10(( the Sorts of U0 . C1))
the Sorts of U0 . C1 is set
K10(( the Sorts of U0 . C1)) is non empty set
{ (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= a1 } is set
union { (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= a1 } is set
a is Element of the carrier of S1
L . a is set
(S1,U0,a) is Element of K10(( the Sorts of U0 . a))
the Sorts of U0 . a is set
K10(( the Sorts of U0 . a)) is non empty set
{ (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= a } is set
union { (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= a } is set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
L is set
B . L is set
B . L is set
G1 is Element of the carrier of S1
B . G1 is set
(S1,U0,G1) is Element of K10(( the Sorts of U0 . G1))
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of U0 . G1 is set
K10(( the Sorts of U0 . G1)) is non empty set
{ (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= G1 } is set
union { (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= G1 } is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
Constants U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is set
(Constants U0) . B is set
(S1,U0) . B is set
B is Element of the carrier of S1
(Constants U0) . B is set
Constants (U0,B) is Element of K10(( the Sorts of U0 . B))
the Sorts of U0 . B is set
K10(( the Sorts of U0 . B)) is non empty set
(S1,U0) . B is set
(S1,U0,B) is Element of K10(( the Sorts of U0 . B))
{ (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= B } is set
union { (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= B } is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
Constants U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is set
(S1,U0) . B is set
B . B is set
G1 is set
L is Element of the carrier of S1
(S1,U0) . L is set
(S1,U0,L) is Element of K10(( the Sorts of U0 . L))
the Sorts of U0 . L is set
K10(( the Sorts of U0 . L)) is non empty set
{ (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= L } is set
union { (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= L } is set
a is set
a1 is Element of the carrier of S1
Constants (U0,a1) is Element of K10(( the Sorts of U0 . a1))
the Sorts of U0 . a1 is set
K10(( the Sorts of U0 . a1)) is non empty set
(Constants U0) . a1 is set
B . a1 is set
B . L is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
Constants U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
(S1,(Constants U0)) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
B is set
L is Element of the carrier of S1
{ ((Constants U0) . b1) where b1 is Element of the carrier of S1 : b1 <= L } is set
{ (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= L } is set
a1 is set
a2 is Element of the carrier of S1
(Constants U0) . a2 is set
Constants (U0,a2) is Element of K10(( the Sorts of U0 . a2))
the Sorts of U0 . a2 is set
K10(( the Sorts of U0 . a2)) is non empty set
a2 is Element of the carrier of S1
Constants (U0,a2) is Element of K10(( the Sorts of U0 . a2))
the Sorts of U0 . a2 is set
K10(( the Sorts of U0 . a2)) is non empty set
(Constants U0) . a2 is set
(S1,U0) . L is set
(S1,U0,L) is Element of K10(( the Sorts of U0 . L))
the Sorts of U0 . L is set
K10(( the Sorts of U0 . L)) is non empty set
union { (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= L } is set
(S1,(Constants U0)) . L is set
(S1,U0) . B is set
(S1,(Constants U0)) . B is set
B is set
(S1,(Constants U0)) . B is set
(S1,U0) . B is set
B is set
(S1,U0) . B is set
(S1,(Constants U0)) . B is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is order-sorted MSSubAlgebra of U0
the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
B is set
(S1,U0) . B is set
the Sorts of B . B is set
Constants U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
G1 is Element of the carrier of S1
(Constants U0) . G1 is set
a is Element of the carrier of S1
the Sorts of B . a is set
the Sorts of B . G1 is set
L is Element of the carrier of S1
{ (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= L } is set
the Sorts of B . L is set
G1 is set
a is Element of the carrier of S1
Constants (U0,a) is Element of K10(( the Sorts of U0 . a))
the Sorts of U0 . a is set
K10(( the Sorts of U0 . a)) is non empty set
(Constants U0) . a is set
(S1,U0,L) is Element of K10(( the Sorts of U0 . L))
the Sorts of U0 . L is set
K10(( the Sorts of U0 . L)) is non empty set
union { (Constants (U0,b1)) where b1 is Element of the carrier of S1 : b1 <= L } is set
S1 is non empty non void V52() all-with_const_op V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is non-empty order-sorted MSAlgebra over S1
(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is non-empty order-sorted MSSubAlgebra of U0
Constants U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set
S1 is set
U0 is Relation-like S1 -defined Function-like V17(S1) set
bool U0 is Relation-like S1 -defined Function-like V17(S1) set
product (bool U0) is set
B is set
dom (bool U0) is set
B is Relation-like S1 -defined Function-like V17(S1) ManySortedSubset of U0
L is set
B . L is set
(bool U0) . L is set
U0 . L is set
bool (U0 . L) is non empty Element of K10(K10((U0 . L)))
K10((U0 . L)) is non empty set
K10(K10((U0 . L))) is non empty set
dom B is set
B is Relation-like Function-like set
dom B is set
L is Relation-like S1 -defined Function-like V17(S1) set
G1 is set
L . G1 is set
U0 . G1 is set
(bool U0) . G1 is set
bool (U0 . G1) is non empty Element of K10(K10((U0 . G1)))
K10((U0 . G1)) is non empty set
K10(K10((U0 . G1))) is non empty set
S1 is non empty V99() V100() V101() RelStr
the carrier of S1 is non empty set
U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
bool U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
product (bool U0) is set
B is set
L is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
SubSort B is non empty set
{ b1 where b1 is Element of SubSort B : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is set
SubSort B is non empty set
{ b1 where b1 is Element of SubSort B : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
B is set
L is Element of SubSort B
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is set
SubSort B is non empty set
{ b1 where b1 is Element of SubSort B : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
B is Element of SubSort B
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is set
SubSort B is non empty set
{ b1 where b1 is Element of SubSort B : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is order-sorted MSAlgebra over S1
SubSort U0 is non empty set
the carrier of S1 is non empty set
{ b1 where b1 is Element of SubSort U0 : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
(S1,U0) is set
SubSort U0 is non empty set
{ b1 where b1 is Element of SubSort U0 : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is non empty set
SubSort B is non empty set
{ b1 where b1 is Element of SubSort B : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
B is set
L is Element of SubSort B
G1 is Element of SubSort U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is order-sorted MSAlgebra over S1
(S1,U0) is set
SubSort U0 is non empty set
the carrier of S1 is non empty set
{ b1 where b1 is Element of SubSort U0 : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
the non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0, the non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)) is non empty set
SubSort the non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0) is non empty set
{ b1 where b1 is Element of SubSort the non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0) : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is order-sorted MSAlgebra over S1
(S1,U0) is non empty set
SubSort U0 is non empty set
the carrier of S1 is non empty set
{ b1 where b1 is Element of SubSort U0 : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
B is Element of (S1,U0)
B is Element of SubSort U0
@ B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is non empty set
SubSort B is non empty set
{ b1 where b1 is Element of SubSort B : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
Constants U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
L is Element of SubSort B
L is Element of SubSort B
Constants U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
(S1,U0) is non empty set
SubSort U0 is non empty set
{ b1 where b1 is Element of SubSort U0 : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is Element of SubSort U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is non empty set
SubSort B is non empty set
{ b1 where b1 is Element of SubSort B : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
B is Element of the carrier of S1
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
Union the Sorts of U0 is set
bool (Union the Sorts of U0) is non empty Element of K10(K10((Union the Sorts of U0)))
K10((Union the Sorts of U0)) is non empty set
K10(K10((Union the Sorts of U0))) is non empty set
G1 is set
rng the Sorts of U0 is non empty set
union (rng the Sorts of U0) is set
bool (union (rng the Sorts of U0)) is non empty Element of K10(K10((union (rng the Sorts of U0))))
K10((union (rng the Sorts of U0))) is non empty set
K10(K10((union (rng the Sorts of U0)))) is non empty set
dom the Sorts of U0 is non empty set
the Sorts of U0 . B is set
a is set
a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
a1 . B is set
a is set
a2 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
a1 is set
a2 . B is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is Element of the carrier of S1
L is Element of the carrier of S1
(S1,U0,B,B) is set
(S1,U0,B,L) is set
G1 is set
(S1,U0,B) is non empty set
SubSort B is non empty set
{ b1 where b1 is Element of SubSort B : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
a . L is set
a . B is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is Element of the carrier of S1
(S1,U0,B,B) is set
SubSort (B,B) is non empty set
L is set
(S1,U0,B) is non empty set
SubSort B is non empty set
{ b1 where b1 is Element of SubSort B : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
G1 . B is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is Element of the carrier of S1
the Sorts of U0 . B is set
(S1,U0,B,B) is set
(S1,U0,B) is non empty set
SubSort B is non empty set
{ b1 where b1 is Element of SubSort B : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
L . B is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is Element of the carrier of S1
(S1,U0,B,B) is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is Relation-like Function-like set
dom B is set
L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
a is set
L . a is set
the Sorts of U0 . a is set
a1 is Element of the carrier of S1
L . a1 is set
(S1,U0,B,a1) is non empty set
meet (S1,U0,B,a1) is set
G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
(S1,U0,B) is non empty set
SubSort B is non empty set
{ b1 where b1 is Element of SubSort B : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
the Sorts of U0 . a1 is set
G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
a1 is Element of the carrier of S1
a2 is Element of the carrier of S1
a . a1 is set
a . a2 is set
(S1,U0,B,a1) is non empty set
meet (S1,U0,B,a1) is set
(S1,U0,B,a2) is non empty set
meet (S1,U0,B,a2) is set
a1 is Element of the carrier of S1
G1 . a1 is set
(S1,U0,B,a1) is non empty set
meet (S1,U0,B,a1) is set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
G1 is set
B . G1 is set
L . G1 is set
a is Element of the carrier of S1
B . a is set
(S1,U0,B,a) is non empty set
meet (S1,U0,B,a) is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
(S1,U0) is non empty set
SubSort U0 is non empty set
{ b1 where b1 is Element of SubSort U0 : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
the Element of (S1,U0) is Element of (S1,U0)
B is Element of SubSort U0
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0) \/ B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is set
((S1,U0) \/ B) . B is set
(S1,U0,B) . B is set
L is Element of the carrier of S1
(S1,U0,B,L) is non empty set
((S1,U0) \/ B) . L is set
G1 is set
(S1,U0,B) is non empty set
SubSort B is non empty set
{ b1 where b1 is Element of SubSort B : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
a . L is set
(S1,U0,B) . L is set
meet (S1,U0,B,L) is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0) \/ B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is set
L is Element of the carrier of S1
(S1,U0,B,L) is non empty set
((S1,U0) \/ B) . L is set
G1 is set
(S1,U0,B) is non empty set
SubSort B is non empty set
{ b1 where b1 is Element of SubSort B : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
a . L is set
meet (S1,U0,B,L) is set
(S1,U0,B) . B is set
G1 is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier' of S1 is non empty set
the carrier of S1 is non empty set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))
the carrier of S1 * is non empty functional V81() M12( the carrier of S1)
K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set
K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set
U0 is order-sorted MSAlgebra over S1
B is Element of the carrier' of S1
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is non empty set
SubSort B is non empty set
{ b1 where b1 is Element of SubSort B : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * ((S1,U0,B) #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
( the Arity of S1 * ((S1,U0,B) #)) . B is set
L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
L # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * (L #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
( the Arity of S1 * (L #)) . B is set
G1 is set
(S1,U0,B) . G1 is set
L . G1 is set
a is Element of the carrier of S1
(S1,U0,B) . a is set
(S1,U0,B,a) is non empty set
meet (S1,U0,B,a) is set
L . a is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier' of S1 is non empty set
the carrier of S1 is non empty set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))
the carrier of S1 * is non empty functional V81() M12( the carrier of S1)
K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set
K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))
K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set
K10(K11( the carrier' of S1, the carrier of S1)) is non empty set
U0 is order-sorted MSAlgebra over S1
B is Element of the carrier' of S1
Den (B,U0) is Relation-like Args (B,U0) -defined Result (B,U0) -valued Function-like V21( Args (B,U0), Result (B,U0)) Element of K10(K11((Args (B,U0)),(Result (B,U0))))
Args (B,U0) is Element of rng ( the Sorts of U0 #)
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of U0 # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
rng ( the Sorts of U0 #) is non empty set
Result (B,U0) is Element of rng the Sorts of U0
rng the Sorts of U0 is non empty set
K11((Args (B,U0)),(Result (B,U0))) is Relation-like set
K10(K11((Args (B,U0)),(Result (B,U0)))) is non empty set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is non empty set
SubSort B is non empty set
{ b1 where b1 is Element of SubSort B : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * ((S1,U0,B) #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
( the Arity of S1 * ((S1,U0,B) #)) . B is set
(Den (B,U0)) | (( the Arity of S1 * ((S1,U0,B) #)) . B) is Relation-like ( the Arity of S1 * ((S1,U0,B) #)) . B -defined Args (B,U0) -defined Result (B,U0) -valued Function-like set
rng ((Den (B,U0)) | (( the Arity of S1 * ((S1,U0,B) #)) . B)) is set
L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
the ResultSort of S1 * L is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
( the ResultSort of S1 * L) . B is set
L # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * (L #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
( the Arity of S1 * (L #)) . B is set
(Den (B,U0)) | (( the Arity of S1 * (L #)) . B) is Relation-like ( the Arity of S1 * (L #)) . B -defined Args (B,U0) -defined Result (B,U0) -valued Function-like set
rng ((Den (B,U0)) | (( the Arity of S1 * (L #)) . B)) is set
(( the Arity of S1 * (L #)) . B) /\ (( the Arity of S1 * ((S1,U0,B) #)) . B) is set
((Den (B,U0)) | (( the Arity of S1 * (L #)) . B)) | (( the Arity of S1 * ((S1,U0,B) #)) . B) is Relation-like ( the Arity of S1 * ((S1,U0,B) #)) . B -defined Args (B,U0) -defined Result (B,U0) -valued Function-like set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier' of S1 is non empty set
the carrier of S1 is non empty set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))
the carrier of S1 * is non empty functional V81() M12( the carrier of S1)
K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set
K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))
K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set
K10(K11( the carrier' of S1, the carrier of S1)) is non empty set
U0 is order-sorted MSAlgebra over S1
B is Element of the carrier' of S1
Den (B,U0) is Relation-like Args (B,U0) -defined Result (B,U0) -valued Function-like V21( Args (B,U0), Result (B,U0)) Element of K10(K11((Args (B,U0)),(Result (B,U0))))
Args (B,U0) is Element of rng ( the Sorts of U0 #)
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of U0 # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
rng ( the Sorts of U0 #) is non empty set
Result (B,U0) is Element of rng the Sorts of U0
rng the Sorts of U0 is non empty set
K11((Args (B,U0)),(Result (B,U0))) is Relation-like set
K10(K11((Args (B,U0)),(Result (B,U0)))) is non empty set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * ((S1,U0,B) #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
( the Arity of S1 * ((S1,U0,B) #)) . B is set
(Den (B,U0)) | (( the Arity of S1 * ((S1,U0,B) #)) . B) is Relation-like ( the Arity of S1 * ((S1,U0,B) #)) . B -defined Args (B,U0) -defined Result (B,U0) -valued Function-like set
rng ((Den (B,U0)) | (( the Arity of S1 * ((S1,U0,B) #)) . B)) is set
the ResultSort of S1 * (S1,U0,B) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
( the ResultSort of S1 * (S1,U0,B)) . B is set
L is set
the_result_sort_of B is Element of the carrier of S1
the ResultSort of S1 . B is set
dom the ResultSort of S1 is set
(S1,U0,B) . (the_result_sort_of B) is set
(S1,U0,B,(the_result_sort_of B)) is non empty set
meet (S1,U0,B,(the_result_sort_of B)) is set
a is set
(S1,U0,B) is non empty set
SubSort B is non empty set
{ b1 where b1 is Element of SubSort B : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
a1 . (the_result_sort_of B) is set
the ResultSort of S1 * a1 is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
( the ResultSort of S1 * a1) . B is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
the carrier' of S1 is non empty set
B is Element of the carrier' of S1
L is Element of the carrier' of S1
Den (L,U0) is Relation-like Args (L,U0) -defined Result (L,U0) -valued Function-like V21( Args (L,U0), Result (L,U0)) Element of K10(K11((Args (L,U0)),(Result (L,U0))))
Args (L,U0) is Element of rng ( the Sorts of U0 #)
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of U0 # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the carrier of S1 * is non empty functional V81() M12( the carrier of S1)
rng ( the Sorts of U0 #) is non empty set
Result (L,U0) is Element of rng the Sorts of U0
rng the Sorts of U0 is non empty set
K11((Args (L,U0)),(Result (L,U0))) is Relation-like set
K10(K11((Args (L,U0)),(Result (L,U0)))) is non empty set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))
K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set
K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set
(S1,U0,B) # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * ((S1,U0,B) #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
( the Arity of S1 * ((S1,U0,B) #)) . L is set
(Den (L,U0)) | (( the Arity of S1 * ((S1,U0,B) #)) . L) is Relation-like ( the Arity of S1 * ((S1,U0,B) #)) . L -defined Args (L,U0) -defined Result (L,U0) -valued Function-like set
rng ((Den (L,U0)) | (( the Arity of S1 * ((S1,U0,B) #)) . L)) is set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))
K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set
K10(K11( the carrier' of S1, the carrier of S1)) is non empty set
the ResultSort of S1 * (S1,U0,B) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
( the ResultSort of S1 * (S1,U0,B)) . L is set
(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0) \/ B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is order-sorted MSAlgebra over S1
the carrier of S1 is non empty set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) opers_closed (S1,U0)
U0 | B is strict MSSubAlgebra of U0
Opers (U0,B) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * (B #), the ResultSort of S1 * B
the carrier' of S1 is non empty set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))
the carrier of S1 * is non empty functional V81() M12( the carrier of S1)
K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set
K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set
B # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * (B #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))
K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set
K10(K11( the carrier' of S1, the carrier of S1)) is non empty set
the ResultSort of S1 * B is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
MSAlgebra(# B,(Opers (U0,B)) #) is strict MSAlgebra over S1
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is order-sorted MSAlgebra over S1
B is order-sorted MSSubAlgebra of U0
B is order-sorted MSSubAlgebra of U0
B /\ B is strict MSSubAlgebra of U0
the carrier of S1 is non empty set
the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
L /\ G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of (B /\ B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) opers_closed (S1,U0)
U0 | (S1,U0,B) is strict order-sorted MSSubAlgebra of U0
L is strict order-sorted MSSubAlgebra of U0
Opers (U0,(S1,U0,B)) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * ((S1,U0,B) #), the ResultSort of S1 * (S1,U0,B)
the carrier' of S1 is non empty set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))
the carrier of S1 * is non empty functional V81() M12( the carrier of S1)
K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set
K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set
(S1,U0,B) # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * ((S1,U0,B) #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))
K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set
K10(K11( the carrier' of S1, the carrier of S1)) is non empty set
the ResultSort of S1 * (S1,U0,B) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
MSAlgebra(# (S1,U0,B),(Opers (U0,(S1,U0,B))) #) is strict MSAlgebra over S1
the Sorts of L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
G1 is order-sorted MSSubAlgebra of U0
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is non empty set
SubSort B is non empty set
{ b1 where b1 is Element of SubSort B : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
a2 is set
the Sorts of L . a2 is set
the Sorts of G1 . a2 is set
a2 is Element of the carrier of S1
the Sorts of L . a2 is set
(S1,U0,B,a2) is non empty set
meet (S1,U0,B,a2) is set
a1 . a2 is set
B is strict order-sorted MSSubAlgebra of U0
L is strict order-sorted MSSubAlgebra of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is strict order-sorted MSSubAlgebra of U0
(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) opers_closed (S1,U0)
U0 | (S1,U0,B) is strict order-sorted MSSubAlgebra of U0
the Sorts of (S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
L is strict order-sorted MSSubAlgebra of U0
Opers (U0,(S1,U0,B)) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * ((S1,U0,B) #), the ResultSort of S1 * (S1,U0,B)
the carrier' of S1 is non empty set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))
the carrier of S1 * is non empty functional V81() M12( the carrier of S1)
K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set
K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set
(S1,U0,B) # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * ((S1,U0,B) #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))
K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set
K10(K11( the carrier' of S1, the carrier of S1)) is non empty set
the ResultSort of S1 * (S1,U0,B) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
MSAlgebra(# (S1,U0,B),(Opers (U0,(S1,U0,B))) #) is strict MSAlgebra over S1
the Sorts of L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
G1 is order-sorted MSSubAlgebra of U0
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is non empty set
SubSort B is non empty set
{ b1 where b1 is Element of SubSort B : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
a2 is set
the Sorts of L . a2 is set
the Sorts of G1 . a2 is set
a2 is Element of the carrier of S1
the Sorts of L . a2 is set
(S1,U0,B,a2) is non empty set
meet (S1,U0,B,a2) is set
a1 . a2 is set
S1 is non empty non void V52() ManySortedSign
the carrier of S1 is non empty set
U0 is MSAlgebra over S1
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
GenMSAlg B is strict MSSubAlgebra of U0
MSSubSort B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
U0 | (MSSubSort B) is strict MSSubAlgebra of U0
the Sorts of (GenMSAlg B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
L is strict MSSubAlgebra of U0
Opers (U0,(MSSubSort B)) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * ((MSSubSort B) #), the ResultSort of S1 * (MSSubSort B)
the carrier' of S1 is non empty set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))
the carrier of S1 * is non empty functional V81() M12( the carrier of S1)
K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set
K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set
(MSSubSort B) # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * ((MSSubSort B) #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))
K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set
K10(K11( the carrier' of S1, the carrier of S1)) is non empty set
the ResultSort of S1 * (MSSubSort B) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
MSAlgebra(# (MSSubSort B),(Opers (U0,(MSSubSort B))) #) is strict MSAlgebra over S1
the Sorts of L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
G1 is MSSubAlgebra of U0
the Sorts of G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
Constants U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
SubSort B is non empty set
a1 is set
the Sorts of L . a1 is set
the Sorts of G1 . a1 is set
a2 is Element of the carrier of S1
the Sorts of L . a2 is set
SubSort (B,a2) is non empty set
meet (SubSort (B,a2)) is set
a . a2 is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
GenMSAlg B is strict MSSubAlgebra of U0
the Sorts of (GenMSAlg B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
(S1,U0,B) is strict order-sorted MSSubAlgebra of U0
the Sorts of (S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
G1 is set
the Sorts of (GenMSAlg B) . G1 is set
the Sorts of (S1,U0,B) . G1 is set
MSSubSort B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
a is Element of the carrier of S1
the Sorts of (GenMSAlg B) . a is set
SubSort (B,a) is non empty set
meet (SubSort (B,a)) is set
(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) opers_closed (S1,U0)
the Sorts of (S1,U0,B) . a is set
(S1,U0,B,a) is non empty set
meet (S1,U0,B,a) is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
GenMSAlg B is strict MSSubAlgebra of U0
(S1,U0,B) is strict order-sorted MSSubAlgebra of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is strict order-sorted MSAlgebra over S1
the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is strict order-sorted MSSubAlgebra of U0
GenMSAlg B is strict MSSubAlgebra of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is order-sorted MSAlgebra over S1
B is strict order-sorted MSSubAlgebra of U0
the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is strict order-sorted MSSubAlgebra of U0
the Sorts of (S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is non-empty order-sorted MSAlgebra over S1
(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
the carrier of S1 is non empty set
(S1,U0,(S1,U0)) is strict order-sorted MSSubAlgebra of U0
B is order-sorted MSSubAlgebra of U0
(S1,U0,(S1,U0)) /\ B is strict order-sorted MSSubAlgebra of U0
the Sorts of (S1,U0,(S1,U0)) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of ((S1,U0,(S1,U0)) /\ B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of (S1,U0,(S1,U0)) /\ the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is non-empty order-sorted MSAlgebra over S1
the carrier of S1 is non empty set
B is order-sorted MSSubAlgebra of U0
the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
B is order-sorted MSSubAlgebra of U0
the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of B \/ the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set
G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
a \/ a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
a2 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,a2) is strict order-sorted MSSubAlgebra of U0
a2 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,a2) is strict order-sorted MSSubAlgebra of U0
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set
a2 is strict order-sorted MSSubAlgebra of U0
a2 is strict order-sorted MSSubAlgebra of U0
a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set
L \/ G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
C1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,C1) is strict order-sorted MSSubAlgebra of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is non-empty order-sorted MSAlgebra over S1
B is order-sorted MSSubAlgebra of U0
the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
B \/ the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
(S1,U0,B) is strict order-sorted MSSubAlgebra of U0
(S1,U0,(S1,U0,B),B) is strict order-sorted MSSubAlgebra of U0
(S1,U0,L) is strict order-sorted MSSubAlgebra of U0
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of (S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
a2 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
a2 \/ a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
a2 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
C1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,C1) is strict order-sorted MSSubAlgebra of U0
the Sorts of (S1,U0,(S1,U0,B),B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
B \/ a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
(S1,U0,B) /\ (S1,U0,L) is strict order-sorted MSSubAlgebra of U0
the Sorts of ((S1,U0,B) /\ (S1,U0,L)) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of (S1,U0,L) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of (S1,U0,B) /\ the Sorts of (S1,U0,L) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is non-empty order-sorted MSAlgebra over S1
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set
B is order-sorted MSSubAlgebra of U0
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is strict order-sorted MSSubAlgebra of U0
(S1,U0,(S1,U0,B),B) is strict order-sorted MSSubAlgebra of U0
the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
B \/ the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is non-empty order-sorted MSAlgebra over S1
B is order-sorted MSSubAlgebra of U0
B is order-sorted MSSubAlgebra of U0
(S1,U0,B,B) is strict order-sorted MSSubAlgebra of U0
(S1,U0,B,B) is strict order-sorted MSSubAlgebra of U0
the carrier of S1 is non empty set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
L \/ G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,a1) is strict order-sorted MSSubAlgebra of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is non-empty order-sorted MSAlgebra over S1
B is strict order-sorted MSSubAlgebra of U0
B is strict order-sorted MSSubAlgebra of U0
(S1,U0,B,B) is strict order-sorted MSSubAlgebra of U0
B /\ (S1,U0,B,B) is strict order-sorted MSSubAlgebra of U0
the carrier of S1 is non empty set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of (B /\ (S1,U0,B,B)) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the carrier' of S1 is non empty set
the Charact of (B /\ (S1,U0,B,B)) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * ( the Sorts of (B /\ (S1,U0,B,B)) #), the ResultSort of S1 * the Sorts of (B /\ (S1,U0,B,B))
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))
the carrier of S1 * is non empty functional V81() M12( the carrier of S1)
K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set
K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set
the Sorts of (B /\ (S1,U0,B,B)) # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * ( the Sorts of (B /\ (S1,U0,B,B)) #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))
K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set
K10(K11( the carrier' of S1, the carrier of S1)) is non empty set
the ResultSort of S1 * the Sorts of (B /\ (S1,U0,B,B)) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
Opers (U0,a) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * (a #), the ResultSort of S1 * a
a # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set
the Arity of S1 * (a #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
the ResultSort of S1 * a is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set
L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
L \/ G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
the Sorts of (S1,U0,B,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of B /\ the Sorts of (S1,U0,B,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
a2 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,a2) is strict order-sorted MSSubAlgebra of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is non-empty order-sorted MSAlgebra over S1
B is strict order-sorted MSSubAlgebra of U0
B is strict order-sorted MSSubAlgebra of U0
B /\ B is strict order-sorted MSSubAlgebra of U0
(S1,U0,(B /\ B),B) is strict order-sorted MSSubAlgebra of U0
the carrier of S1 is non empty set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of (B /\ B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
a \/ a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
a2 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of B /\ the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
a2 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,a2) is strict order-sorted MSSubAlgebra of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is order-sorted MSAlgebra over S1
(S1,U0) is non empty set
SubSort U0 is non empty set
the carrier of S1 is non empty set
{ b1 where b1 is Element of SubSort U0 : b1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set } is set
{ (S1,U0,(S1,U0,b1)) where b1 is Element of (S1,U0) : verum } is set
B is set
L is Element of (S1,U0)
(S1,U0,L) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,(S1,U0,L)) is strict order-sorted MSSubAlgebra of U0
L is strict order-sorted MSSubAlgebra of U0
the Sorts of L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
a is Element of (S1,U0)
(S1,U0,a) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,(S1,U0,a)) is strict order-sorted MSSubAlgebra of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is order-sorted MSAlgebra over S1
(S1,U0) is set
MSSub U0 is non empty set
B is set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is order-sorted MSAlgebra over S1
(S1,U0) is set
the strict order-sorted MSSubAlgebra of U0 is strict order-sorted MSSubAlgebra of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is order-sorted MSAlgebra over S1
(S1,U0) is non empty set
MSSub U0 is non empty set
K10((MSSub U0)) is non empty set
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is non-empty order-sorted MSAlgebra over S1
(S1,U0) is non empty Element of K10((MSSub U0))
MSSub U0 is non empty set
K10((MSSub U0)) is non empty set
K11((S1,U0),(S1,U0)) is non empty Relation-like set
K11(K11((S1,U0),(S1,U0)),(S1,U0)) is non empty Relation-like set
K10(K11(K11((S1,U0),(S1,U0)),(S1,U0))) is non empty set
B is Element of (S1,U0)
B is Element of (S1,U0)
L is strict order-sorted MSSubAlgebra of U0
G1 is strict order-sorted MSSubAlgebra of U0
(S1,U0,L,G1) is strict order-sorted MSSubAlgebra of U0
a is Element of (S1,U0)
a1 is strict order-sorted MSSubAlgebra of U0
a2 is strict order-sorted MSSubAlgebra of U0
(S1,U0,a1,a2) is strict order-sorted MSSubAlgebra of U0
B is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
B is Element of (S1,U0)
G1 is strict order-sorted MSSubAlgebra of U0
L is Element of (S1,U0)
a is strict order-sorted MSSubAlgebra of U0
B . (B,L) is Element of (S1,U0)
(S1,U0,G1,a) is strict order-sorted MSSubAlgebra of U0
B is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
B is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
L is Element of (S1,U0)
G1 is Element of (S1,U0)
B . (L,G1) is Element of (S1,U0)
B . (L,G1) is Element of (S1,U0)
a is strict order-sorted MSSubAlgebra of U0
a1 is strict order-sorted MSSubAlgebra of U0
(S1,U0,a,a1) is strict order-sorted MSSubAlgebra of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is non-empty order-sorted MSAlgebra over S1
(S1,U0) is non empty Element of K10((MSSub U0))
MSSub U0 is non empty set
K10((MSSub U0)) is non empty set
K11((S1,U0),(S1,U0)) is non empty Relation-like set
K11(K11((S1,U0),(S1,U0)),(S1,U0)) is non empty Relation-like set
K10(K11(K11((S1,U0),(S1,U0)),(S1,U0))) is non empty set
B is Element of (S1,U0)
B is Element of (S1,U0)
L is strict order-sorted MSSubAlgebra of U0
G1 is strict order-sorted MSSubAlgebra of U0
L /\ G1 is strict order-sorted MSSubAlgebra of U0
a is Element of (S1,U0)
a1 is strict order-sorted MSSubAlgebra of U0
a2 is strict order-sorted MSSubAlgebra of U0
a1 /\ a2 is strict order-sorted MSSubAlgebra of U0
B is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
B is Element of (S1,U0)
G1 is strict order-sorted MSSubAlgebra of U0
L is Element of (S1,U0)
a is strict order-sorted MSSubAlgebra of U0
B . (B,L) is Element of (S1,U0)
G1 /\ a is strict order-sorted MSSubAlgebra of U0
B is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
B is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
L is Element of (S1,U0)
G1 is Element of (S1,U0)
B . (L,G1) is Element of (S1,U0)
B . (L,G1) is Element of (S1,U0)
a is strict order-sorted MSSubAlgebra of U0
a1 is strict order-sorted MSSubAlgebra of U0
a /\ a1 is strict order-sorted MSSubAlgebra of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is non-empty order-sorted MSAlgebra over S1
MSSub U0 is non empty set
(S1,U0) is non empty Element of K10((MSSub U0))
K10((MSSub U0)) is non empty set
(S1,U0) is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
K11((S1,U0),(S1,U0)) is non empty Relation-like set
K11(K11((S1,U0),(S1,U0)),(S1,U0)) is non empty Relation-like set
K10(K11(K11((S1,U0),(S1,U0)),(S1,U0))) is non empty set
MSAlg_meet U0 is Relation-like K11((MSSub U0),(MSSub U0)) -defined MSSub U0 -valued Function-like V21(K11((MSSub U0),(MSSub U0)), MSSub U0) Element of K10(K11(K11((MSSub U0),(MSSub U0)),(MSSub U0)))
K11((MSSub U0),(MSSub U0)) is non empty Relation-like set
K11(K11((MSSub U0),(MSSub U0)),(MSSub U0)) is non empty Relation-like set
K10(K11(K11((MSSub U0),(MSSub U0)),(MSSub U0))) is non empty set
B is Element of (S1,U0)
B is Element of (S1,U0)
(S1,U0) . (B,B) is Element of (S1,U0)
(MSAlg_meet U0) . (B,B) is Element of MSSub U0
L is strict order-sorted MSSubAlgebra of U0
G1 is strict order-sorted MSSubAlgebra of U0
L /\ G1 is strict order-sorted MSSubAlgebra of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is non-empty order-sorted MSAlgebra over S1
(S1,U0) is non empty Element of K10((MSSub U0))
MSSub U0 is non empty set
K10((MSSub U0)) is non empty set
(S1,U0) is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
K11((S1,U0),(S1,U0)) is non empty Relation-like set
K11(K11((S1,U0),(S1,U0)),(S1,U0)) is non empty Relation-like set
K10(K11(K11((S1,U0),(S1,U0)),(S1,U0))) is non empty set
B is Element of (S1,U0)
L is Element of (S1,U0)
(S1,U0) . (B,L) is Element of (S1,U0)
(S1,U0) . (L,B) is Element of (S1,U0)
the carrier of S1 is non empty set
G1 is strict order-sorted MSSubAlgebra of U0
the Sorts of G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
a is strict order-sorted MSSubAlgebra of U0
the Sorts of a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of G1 \/ the Sorts of a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set
(S1,U0,G1,a) is strict order-sorted MSSubAlgebra of U0
a2 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,a2) is strict order-sorted MSSubAlgebra of U0
(S1,U0,a,G1) is strict order-sorted MSSubAlgebra of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is non-empty order-sorted MSAlgebra over S1
(S1,U0) is non empty Element of K10((MSSub U0))
MSSub U0 is non empty set
K10((MSSub U0)) is non empty set
(S1,U0) is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
K11((S1,U0),(S1,U0)) is non empty Relation-like set
K11(K11((S1,U0),(S1,U0)),(S1,U0)) is non empty Relation-like set
K10(K11(K11((S1,U0),(S1,U0)),(S1,U0))) is non empty set
B is Element of (S1,U0)
L is Element of (S1,U0)
G1 is Element of (S1,U0)
(S1,U0) . (L,G1) is Element of (S1,U0)
(S1,U0) . (B,((S1,U0) . (L,G1))) is Element of (S1,U0)
(S1,U0) . (B,L) is Element of (S1,U0)
(S1,U0) . (((S1,U0) . (B,L)),G1) is Element of (S1,U0)
the carrier of S1 is non empty set
a is strict order-sorted MSSubAlgebra of U0
the Sorts of a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
a1 is strict order-sorted MSSubAlgebra of U0
the Sorts of a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
a2 is strict order-sorted MSSubAlgebra of U0
the Sorts of a2 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of a1 \/ the Sorts of a2 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of a \/ ( the Sorts of a1 \/ the Sorts of a2) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set
C1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
the Sorts of a \/ the Sorts of a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
(S1,U0,a1,a2) is strict order-sorted MSSubAlgebra of U0
(S1,U0,a,(S1,U0,a1,a2)) is strict order-sorted MSSubAlgebra of U0
D1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
(S1,U0,a,a1) is strict order-sorted MSSubAlgebra of U0
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
D is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
D \/ the Sorts of a2 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set
(S1,U0,(S1,U0,a,a1),a2) is strict order-sorted MSSubAlgebra of U0
(S1,U0,D) is strict order-sorted MSSubAlgebra of U0
(S1,U0,(S1,U0,D),a2) is strict order-sorted MSSubAlgebra of U0
(S1,U0,B) is strict order-sorted MSSubAlgebra of U0
C is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,C) is strict order-sorted MSSubAlgebra of U0
(S1,U0,a,(S1,U0,C)) is strict order-sorted MSSubAlgebra of U0
(S1,U0,(S1,U0,C),a) is strict order-sorted MSSubAlgebra of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is non-empty order-sorted MSAlgebra over S1
(S1,U0) is non empty Element of K10((MSSub U0))
MSSub U0 is non empty set
K10((MSSub U0)) is non empty set
(S1,U0) is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
K11((S1,U0),(S1,U0)) is non empty Relation-like set
K11(K11((S1,U0),(S1,U0)),(S1,U0)) is non empty Relation-like set
K10(K11(K11((S1,U0),(S1,U0)),(S1,U0))) is non empty set
MSAlg_meet U0 is Relation-like K11((MSSub U0),(MSSub U0)) -defined MSSub U0 -valued Function-like V21(K11((MSSub U0),(MSSub U0)), MSSub U0) Element of K10(K11(K11((MSSub U0),(MSSub U0)),(MSSub U0)))
K11((MSSub U0),(MSSub U0)) is non empty Relation-like set
K11(K11((MSSub U0),(MSSub U0)),(MSSub U0)) is non empty Relation-like set
K10(K11(K11((MSSub U0),(MSSub U0)),(MSSub U0))) is non empty set
L is Element of (S1,U0)
G1 is Element of (S1,U0)
(S1,U0) . (L,G1) is Element of (S1,U0)
(S1,U0) . (G1,L) is Element of (S1,U0)
(MSAlg_meet U0) . (L,G1) is Element of MSSub U0
(MSAlg_meet U0) . (G1,L) is Element of MSSub U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is non-empty order-sorted MSAlgebra over S1
(S1,U0) is non empty Element of K10((MSSub U0))
MSSub U0 is non empty set
K10((MSSub U0)) is non empty set
(S1,U0) is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
K11((S1,U0),(S1,U0)) is non empty Relation-like set
K11(K11((S1,U0),(S1,U0)),(S1,U0)) is non empty Relation-like set
K10(K11(K11((S1,U0),(S1,U0)),(S1,U0))) is non empty set
MSAlg_meet U0 is Relation-like K11((MSSub U0),(MSSub U0)) -defined MSSub U0 -valued Function-like V21(K11((MSSub U0),(MSSub U0)), MSSub U0) Element of K10(K11(K11((MSSub U0),(MSSub U0)),(MSSub U0)))
K11((MSSub U0),(MSSub U0)) is non empty Relation-like set
K11(K11((MSSub U0),(MSSub U0)),(MSSub U0)) is non empty Relation-like set
K10(K11(K11((MSSub U0),(MSSub U0)),(MSSub U0))) is non empty set
L is Element of (S1,U0)
G1 is Element of (S1,U0)
a is Element of (S1,U0)
(S1,U0) . (G1,a) is Element of (S1,U0)
(S1,U0) . (L,((S1,U0) . (G1,a))) is Element of (S1,U0)
(S1,U0) . (L,G1) is Element of (S1,U0)
(S1,U0) . (((S1,U0) . (L,G1)),a) is Element of (S1,U0)
(MSAlg_meet U0) . (L,G1) is Element of MSSub U0
(MSAlg_meet U0) . (G1,a) is Element of MSSub U0
(MSAlg_meet U0) . (L,((MSAlg_meet U0) . (G1,a))) is Element of MSSub U0
(MSAlg_meet U0) . (((MSAlg_meet U0) . (L,G1)),a) is Element of MSSub U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is non-empty order-sorted MSAlgebra over S1
(S1,U0) is non empty Element of K10((MSSub U0))
MSSub U0 is non empty set
K10((MSSub U0)) is non empty set
(S1,U0) is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
K11((S1,U0),(S1,U0)) is non empty Relation-like set
K11(K11((S1,U0),(S1,U0)),(S1,U0)) is non empty Relation-like set
K10(K11(K11((S1,U0),(S1,U0)),(S1,U0))) is non empty set
(S1,U0) is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
LattStr(# (S1,U0),(S1,U0),(S1,U0) #) is non empty strict LattStr
the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) is non empty set
B is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
L is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
G1 is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
L "\/" G1 is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
the L_join of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) is Relation-like K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) -defined the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) -valued Function-like V21(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) Element of K10(K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)))
K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) is non empty Relation-like set
K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) is non empty Relation-like set
K10(K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #))) is non empty set
the L_join of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) . (L,G1) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
B "\/" (L "\/" G1) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
the L_join of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) . (B,(L "\/" G1)) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
B "\/" L is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
the L_join of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) . (B,L) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
(B "\/" L) "\/" G1 is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
the L_join of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) . ((B "\/" L),G1) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
B is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
L is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
B "/\" L is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
the L_meet of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) is Relation-like K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) -defined the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) -valued Function-like V21(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) Element of K10(K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)))
K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) is non empty Relation-like set
K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) is non empty Relation-like set
K10(K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #))) is non empty set
the L_meet of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) . (B,L) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
L "/\" B is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
the L_meet of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) . (L,B) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
B is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
L is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
B "\/" L is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
the L_join of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) is Relation-like K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) -defined the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) -valued Function-like V21(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) Element of K10(K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)))
K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) is non empty Relation-like set
K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) is non empty Relation-like set
K10(K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #))) is non empty set
the L_join of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) . (B,L) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
B "/\" (B "\/" L) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
the L_meet of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) is Relation-like K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) -defined the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) -valued Function-like V21(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) Element of K10(K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)))
the L_meet of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) . (B,(B "\/" L)) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
G1 is Element of (S1,U0)
a is Element of (S1,U0)
(S1,U0) . (G1,a) is Element of (S1,U0)
(S1,U0) . (G1,((S1,U0) . (G1,a))) is Element of (S1,U0)
a1 is strict order-sorted MSSubAlgebra of U0
a2 is strict order-sorted MSSubAlgebra of U0
(S1,U0,a1,a2) is strict order-sorted MSSubAlgebra of U0
a1 /\ (S1,U0,a1,a2) is strict order-sorted MSSubAlgebra of U0
B is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
L is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
B "/\" L is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
the L_meet of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) is Relation-like K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) -defined the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) -valued Function-like V21(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) Element of K10(K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)))
K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) is non empty Relation-like set
K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) is non empty Relation-like set
K10(K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #))) is non empty set
the L_meet of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) . (B,L) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
(B "/\" L) "\/" L is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
the L_join of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) is Relation-like K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) -defined the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) -valued Function-like V21(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) Element of K10(K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)))
the L_join of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) . ((B "/\" L),L) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
G1 is Element of (S1,U0)
a is Element of (S1,U0)
(S1,U0) . (G1,a) is Element of (S1,U0)
(S1,U0) . (((S1,U0) . (G1,a)),a) is Element of (S1,U0)
a1 is strict order-sorted MSSubAlgebra of U0
a2 is strict order-sorted MSSubAlgebra of U0
a1 /\ a2 is strict order-sorted MSSubAlgebra of U0
(S1,U0,(a1 /\ a2),a2) is strict order-sorted MSSubAlgebra of U0
B is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
L is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
G1 is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
L "/\" G1 is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
the L_meet of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) is Relation-like K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) -defined the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) -valued Function-like V21(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) Element of K10(K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)))
K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) is non empty Relation-like set
K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) is non empty Relation-like set
K10(K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #))) is non empty set
the L_meet of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) . (L,G1) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
B "/\" (L "/\" G1) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
the L_meet of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) . (B,(L "/\" G1)) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
B "/\" L is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
the L_meet of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) . (B,L) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
(B "/\" L) "/\" G1 is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
the L_meet of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) . ((B "/\" L),G1) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
B is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
L is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
B "\/" L is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
the L_join of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) is Relation-like K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) -defined the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) -valued Function-like V21(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) Element of K10(K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)))
K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) is non empty Relation-like set
K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)) is non empty Relation-like set
K10(K11(K11( the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)), the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #))) is non empty set
the L_join of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) . (B,L) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
L "\/" B is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
the L_join of LattStr(# (S1,U0),(S1,U0),(S1,U0) #) . (L,B) is Element of the carrier of LattStr(# (S1,U0),(S1,U0),(S1,U0) #)
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is non-empty order-sorted MSAlgebra over S1
(S1,U0) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(S1,U0) is non empty Element of K10((MSSub U0))
MSSub U0 is non empty set
K10((MSSub U0)) is non empty set
(S1,U0) is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
K11((S1,U0),(S1,U0)) is non empty Relation-like set
K11(K11((S1,U0),(S1,U0)),(S1,U0)) is non empty Relation-like set
K10(K11(K11((S1,U0),(S1,U0)),(S1,U0))) is non empty set
(S1,U0) is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
LattStr(# (S1,U0),(S1,U0),(S1,U0) #) is non empty strict LattStr
(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
the carrier of S1 is non empty set
(S1,U0,(S1,U0)) is strict order-sorted MSSubAlgebra of U0
the carrier of (S1,U0) is non empty set
L is Element of (S1,U0)
G1 is Element of the carrier of (S1,U0)
a is Element of the carrier of (S1,U0)
G1 "/\" a is Element of the carrier of (S1,U0)
the L_meet of (S1,U0) is Relation-like K11( the carrier of (S1,U0), the carrier of (S1,U0)) -defined the carrier of (S1,U0) -valued Function-like V21(K11( the carrier of (S1,U0), the carrier of (S1,U0)), the carrier of (S1,U0)) Element of K10(K11(K11( the carrier of (S1,U0), the carrier of (S1,U0)), the carrier of (S1,U0)))
K11( the carrier of (S1,U0), the carrier of (S1,U0)) is non empty Relation-like set
K11(K11( the carrier of (S1,U0), the carrier of (S1,U0)), the carrier of (S1,U0)) is non empty Relation-like set
K10(K11(K11( the carrier of (S1,U0), the carrier of (S1,U0)), the carrier of (S1,U0))) is non empty set
the L_meet of (S1,U0) . (G1,a) is Element of the carrier of (S1,U0)
a "/\" G1 is Element of the carrier of (S1,U0)
the L_meet of (S1,U0) . (a,G1) is Element of the carrier of (S1,U0)
a1 is Element of (S1,U0)
G1 "/\" a is Element of the carrier of (S1,U0)
a2 is strict order-sorted MSSubAlgebra of U0
(S1,U0,(S1,U0)) /\ a2 is strict order-sorted MSSubAlgebra of U0
the carrier of S1 is non empty set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,L) is strict order-sorted MSSubAlgebra of U0
the carrier of (S1,U0) is non empty set
G1 is Element of (S1,U0)
a is Element of the carrier of (S1,U0)
a1 is Element of the carrier of (S1,U0)
a "\/" a1 is Element of the carrier of (S1,U0)
the L_join of (S1,U0) is Relation-like K11( the carrier of (S1,U0), the carrier of (S1,U0)) -defined the carrier of (S1,U0) -valued Function-like V21(K11( the carrier of (S1,U0), the carrier of (S1,U0)), the carrier of (S1,U0)) Element of K10(K11(K11( the carrier of (S1,U0), the carrier of (S1,U0)), the carrier of (S1,U0)))
K11( the carrier of (S1,U0), the carrier of (S1,U0)) is non empty Relation-like set
K11(K11( the carrier of (S1,U0), the carrier of (S1,U0)), the carrier of (S1,U0)) is non empty Relation-like set
K10(K11(K11( the carrier of (S1,U0), the carrier of (S1,U0)), the carrier of (S1,U0))) is non empty set
the L_join of (S1,U0) . (a,a1) is Element of the carrier of (S1,U0)
a1 "\/" a is Element of the carrier of (S1,U0)
the L_join of (S1,U0) . (a1,a) is Element of the carrier of (S1,U0)
a2 is Element of (S1,U0)
a "\/" a1 is Element of the carrier of (S1,U0)
a2 is strict order-sorted MSSubAlgebra of U0
(S1,U0,(S1,U0,L),a2) is strict order-sorted MSSubAlgebra of U0
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is non-empty order-sorted MSAlgebra over S1
(S1,U0) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(S1,U0) is non empty Element of K10((MSSub U0))
MSSub U0 is non empty set
K10((MSSub U0)) is non empty set
(S1,U0) is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
K11((S1,U0),(S1,U0)) is non empty Relation-like set
K11(K11((S1,U0),(S1,U0)),(S1,U0)) is non empty Relation-like set
K10(K11(K11((S1,U0),(S1,U0)),(S1,U0))) is non empty set
(S1,U0) is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
LattStr(# (S1,U0),(S1,U0),(S1,U0) #) is non empty strict LattStr
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is non-empty order-sorted MSAlgebra over S1
(S1,U0) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
(S1,U0) is non empty Element of K10((MSSub U0))
MSSub U0 is non empty set
K10((MSSub U0)) is non empty set
(S1,U0) is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
K11((S1,U0),(S1,U0)) is non empty Relation-like set
K11(K11((S1,U0),(S1,U0)),(S1,U0)) is non empty Relation-like set
K10(K11(K11((S1,U0),(S1,U0)),(S1,U0))) is non empty set
(S1,U0) is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
LattStr(# (S1,U0),(S1,U0),(S1,U0) #) is non empty strict LattStr
Bottom (S1,U0) is Element of the carrier of (S1,U0)
the carrier of (S1,U0) is non empty set
(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
the carrier of S1 is non empty set
(S1,U0,(S1,U0)) is strict order-sorted MSSubAlgebra of U0
B is Element of (S1,U0)
a is Element of the carrier of (S1,U0)
a1 is Element of (S1,U0)
G1 is Element of the carrier of (S1,U0)
G1 "/\" a is Element of the carrier of (S1,U0)
the L_meet of (S1,U0) is Relation-like K11( the carrier of (S1,U0), the carrier of (S1,U0)) -defined the carrier of (S1,U0) -valued Function-like V21(K11( the carrier of (S1,U0), the carrier of (S1,U0)), the carrier of (S1,U0)) Element of K10(K11(K11( the carrier of (S1,U0), the carrier of (S1,U0)), the carrier of (S1,U0)))
K11( the carrier of (S1,U0), the carrier of (S1,U0)) is non empty Relation-like set
K11(K11( the carrier of (S1,U0), the carrier of (S1,U0)), the carrier of (S1,U0)) is non empty Relation-like set
K10(K11(K11( the carrier of (S1,U0), the carrier of (S1,U0)), the carrier of (S1,U0))) is non empty set
the L_meet of (S1,U0) . (G1,a) is Element of the carrier of (S1,U0)
a2 is strict order-sorted MSSubAlgebra of U0
(S1,U0,(S1,U0)) /\ a2 is strict order-sorted MSSubAlgebra of U0
a "/\" G1 is Element of the carrier of (S1,U0)
the L_meet of (S1,U0) . (a,G1) is Element of the carrier of (S1,U0)
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
the carrier of S1 is non empty set
U0 is non-empty order-sorted MSAlgebra over S1
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set
(S1,U0) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
(S1,U0) is non empty Element of K10((MSSub U0))
MSSub U0 is non empty set
K10((MSSub U0)) is non empty set
(S1,U0) is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
K11((S1,U0),(S1,U0)) is non empty Relation-like set
K11(K11((S1,U0),(S1,U0)),(S1,U0)) is non empty Relation-like set
K10(K11(K11((S1,U0),(S1,U0)),(S1,U0))) is non empty set
(S1,U0) is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
LattStr(# (S1,U0),(S1,U0),(S1,U0) #) is non empty strict LattStr
Top (S1,U0) is Element of the carrier of (S1,U0)
the carrier of (S1,U0) is non empty set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is strict order-sorted MSSubAlgebra of U0
B is Element of (S1,U0)
a is Element of the carrier of (S1,U0)
a1 is Element of (S1,U0)
G1 is Element of the carrier of (S1,U0)
G1 "\/" a is Element of the carrier of (S1,U0)
the L_join of (S1,U0) is Relation-like K11( the carrier of (S1,U0), the carrier of (S1,U0)) -defined the carrier of (S1,U0) -valued Function-like V21(K11( the carrier of (S1,U0), the carrier of (S1,U0)), the carrier of (S1,U0)) Element of K10(K11(K11( the carrier of (S1,U0), the carrier of (S1,U0)), the carrier of (S1,U0)))
K11( the carrier of (S1,U0), the carrier of (S1,U0)) is non empty Relation-like set
K11(K11( the carrier of (S1,U0), the carrier of (S1,U0)), the carrier of (S1,U0)) is non empty Relation-like set
K10(K11(K11( the carrier of (S1,U0), the carrier of (S1,U0)), the carrier of (S1,U0))) is non empty set
the L_join of (S1,U0) . (G1,a) is Element of the carrier of (S1,U0)
a2 is strict order-sorted MSSubAlgebra of U0
(S1,U0,(S1,U0,B),a2) is strict order-sorted MSSubAlgebra of U0
a "\/" G1 is Element of the carrier of (S1,U0)
the L_join of (S1,U0) . (a,G1) is Element of the carrier of (S1,U0)
S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign
U0 is strict non-empty order-sorted MSAlgebra over S1
(S1,U0) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
(S1,U0) is non empty Element of K10((MSSub U0))
MSSub U0 is non empty set
K10((MSSub U0)) is non empty set
(S1,U0) is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
K11((S1,U0),(S1,U0)) is non empty Relation-like set
K11(K11((S1,U0),(S1,U0)),(S1,U0)) is non empty Relation-like set
K10(K11(K11((S1,U0),(S1,U0)),(S1,U0))) is non empty set
(S1,U0) is Relation-like K11((S1,U0),(S1,U0)) -defined (S1,U0) -valued Function-like V21(K11((S1,U0),(S1,U0)),(S1,U0)) Element of K10(K11(K11((S1,U0),(S1,U0)),(S1,U0)))
LattStr(# (S1,U0),(S1,U0),(S1,U0) #) is non empty strict LattStr
Top (S1,U0) is Element of the carrier of (S1,U0)
the carrier of (S1,U0) is non empty set
the carrier of S1 is non empty set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0
B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)
(S1,U0,B) is strict order-sorted MSSubAlgebra of U0