NAT is non empty V27() V28() V29() V34() V39() V40() Element of K19(REAL)
REAL is set
K19(REAL) is non empty set
NAT is non empty V27() V28() V29() V34() V39() V40() set
K19(NAT) is non empty V34() set
K19(NAT) is non empty V34() set
K279() is set
{} is functional empty V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-membered set
the functional empty V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-membered set is functional empty V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-membered set
1 is non empty set
2 is non empty set
3 is non empty set
0 is functional empty V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-membered Element of NAT
U0 is non empty V108() V109() non-empty UAStr
F is set
U0 is non empty V108() V109() non-empty UAStr
the non empty V108() V109() non-empty SubAlgebra of U0 is non empty V108() V109() non-empty SubAlgebra of U0
{ the non empty V108() V109() non-empty SubAlgebra of U0} is non empty trivial V41(1) set
a is set
a is (U0)
U0 is non empty V108() V109() non-empty UAStr
Sub U0 is non empty set
F is set
F is non empty (U0)
a is Element of F
U0 is non empty V108() V109() non-empty UAStr
(U0) is non empty (U0)
the carrier of U0 is non empty set
K19( the carrier of U0) is non empty set
F is non empty V108() V109() non-empty (U0,(U0))
a is non empty V108() V109() non-empty SubAlgebra of U0
the carrier of a is non empty set
a is Element of K19( the carrier of U0)
H1 is non empty V108() V109() non-empty SubAlgebra of U0
a is Element of K19( the carrier of U0)
the carrier of H1 is non empty set
a1 is non empty V108() V109() non-empty SubAlgebra of U0
a is Element of K19( the carrier of U0)
the carrier of a1 is non empty set
U0 is non empty V108() V109() non-empty UAStr
(U0) is non empty (U0)
the carrier of U0 is non empty set
bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))
K19( the carrier of U0) is non empty set
K19(K19( the carrier of U0)) is non empty set
K20((U0),(bool the carrier of U0)) is non empty set
K19(K20((U0),(bool the carrier of U0))) is non empty set
F is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))
F is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))
a is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))
a is set
F . a is set
a . a is set
H1 is non empty V108() V109() non-empty (U0,(U0))
(U0,H1) is Element of K19( the carrier of U0)
a1 is non empty V108() V109() non-empty SubAlgebra of U0
the carrier of a1 is non empty set
F . H1 is Element of bool the carrier of U0
U0 is non empty V108() V109() non-empty UAStr
(U0) is non empty (U0)
F is set
a is non empty strict V108() V109() non-empty SubAlgebra of U0
U0 is non empty V108() V109() non-empty UAStr
the carrier of U0 is non empty set
K19( the carrier of U0) is non empty set
the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0
Operations U0 is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)
K36(( the carrier of U0 *), the carrier of U0) is set
rng the charact of U0 is set
F is non empty Element of K19( the carrier of U0)
a is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0
arity a is V27() V28() V29() V33() V34() V39() Element of NAT
a . {} is set
a is Relation-like NAT -defined F -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of F
len a is V27() V28() V29() V33() V34() V39() Element of NAT
a is Relation-like NAT -defined F -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of F
len a is V27() V28() V29() V33() V34() V39() Element of NAT
a . a is set
U0 is non empty V108() V109() non-empty UAStr
the carrier of U0 is non empty set
F is non empty V108() V109() non-empty SubAlgebra of U0
the carrier of F is non empty set
K19( the carrier of U0) is non empty set
U0 is non empty V108() V109() non-empty UAStr
the carrier of U0 is non empty set
K19( the carrier of U0) is non empty set
the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0
Operations U0 is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)
K36(( the carrier of U0 *), the carrier of U0) is set
rng the charact of U0 is set
F is non empty Element of K19( the carrier of U0)
a is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0
arity a is V27() V28() V29() V33() V34() V39() Element of NAT
a /. F is Relation-like F * -defined F -valued Function-like non empty homogeneous V119(F) Element of K19(K20((F *),F))
F * is functional non empty FinSequence-membered FinSequenceSet of F
K20((F *),F) is non empty set
K19(K20((F *),F)) is non empty set
dom a is functional FinSequence-membered Element of K19(( the carrier of U0 *))
K19(( the carrier of U0 *)) is non empty set
0 -tuples_on the carrier of U0 is FinSequenceSet of the carrier of U0
<*> the carrier of U0 is Relation-like NAT -defined the carrier of U0 -valued Function-like functional empty proper V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of U0
K20(NAT, the carrier of U0) is non empty V34() set
{(<*> the carrier of U0)} is non empty trivial V41(1) set
<*> F is Relation-like NAT -defined F -valued Function-like functional empty proper V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of F
K20(NAT,F) is non empty V34() set
{(<*> F)} is non empty trivial V41(1) set
0 -tuples_on F is FinSequenceSet of F
a | (0 -tuples_on F) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Element of K19(K20(( the carrier of U0 *), the carrier of U0))
K20(( the carrier of U0 *), the carrier of U0) is non empty set
K19(K20(( the carrier of U0 *), the carrier of U0)) is non empty set
U0 is non empty V108() V109() non-empty UAStr
Constants U0 is Element of K19( the carrier of U0)
the carrier of U0 is non empty set
K19( the carrier of U0) is non empty set
the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0
Operations U0 is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)
K36(( the carrier of U0 *), the carrier of U0) is set
rng the charact of U0 is set
{ b1 where b1 is Element of the carrier of U0 : ex b2 being Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0 st
( arity b2 = 0 & b1 in rng b2 ) } is set
{ (b1 . {}) where b1 is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0 : arity b1 = 0 } is set
a is set
a is Element of the carrier of U0
H1 is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0
arity H1 is V27() V28() V29() V33() V34() V39() Element of NAT
rng H1 is Element of K19( the carrier of U0)
H1 is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0
arity H1 is V27() V28() V29() V33() V34() V39() Element of NAT
rng H1 is Element of K19( the carrier of U0)
dom H1 is functional FinSequence-membered Element of K19(( the carrier of U0 *))
K19(( the carrier of U0 *)) is non empty set
a1 is set
H1 . a1 is set
0 -tuples_on the carrier of U0 is FinSequenceSet of the carrier of U0
K20(NAT, the carrier of U0) is non empty V34() set
U1 is Relation-like NAT -defined the carrier of U0 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of the carrier of U0
len U1 is V27() V28() V29() V33() V34() V39() Element of NAT
a is set
a is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0
a . {} is set
arity a is V27() V28() V29() V33() V34() V39() Element of NAT
dom a is functional FinSequence-membered Element of K19(( the carrier of U0 *))
K19(( the carrier of U0 *)) is non empty set
0 -tuples_on the carrier of U0 is FinSequenceSet of the carrier of U0
<*> the carrier of U0 is Relation-like NAT -defined the carrier of U0 -valued Function-like functional empty proper V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of U0
K20(NAT, the carrier of U0) is non empty V34() set
{(<*> the carrier of U0)} is non empty trivial V41(1) set
{} the carrier of U0 is functional empty proper V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-membered Element of K19( the carrier of U0)
a . ({} the carrier of U0) is set
rng a is Element of K19( the carrier of U0)
U0 is non empty V108() V109() non-empty with_const_op UAStr
Constants U0 is non empty Element of K19( the carrier of U0)
the carrier of U0 is non empty set
K19( the carrier of U0) is non empty set
the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0
Operations U0 is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)
K36(( the carrier of U0 *), the carrier of U0) is set
rng the charact of U0 is set
{ b1 where b1 is Element of the carrier of U0 : ex b2 being Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0 st
( arity b2 = 0 & b1 in rng b2 ) } is set
F is non empty V108() V109() non-empty SubAlgebra of U0
Constants F is Element of K19( the carrier of F)
the carrier of F is non empty set
K19( the carrier of F) is non empty set
the carrier of F * is functional non empty FinSequence-membered FinSequenceSet of the carrier of F
Operations F is non empty PFuncsDomHQN of the carrier of F
the charact of F is Relation-like NAT -defined K36(( the carrier of F *), the carrier of F) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of F *), the carrier of F)
K36(( the carrier of F *), the carrier of F) is set
rng the charact of F is set
{ b1 where b1 is Element of the carrier of F : ex b2 being Relation-like the carrier of F * -defined the carrier of F -valued Function-like non empty homogeneous V119( the carrier of F) Element of Operations F st
( arity b2 = 0 & b1 in rng b2 ) } is set
a is set
H1 is Element of the carrier of U0
a1 is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0
arity a1 is V27() V28() V29() V33() V34() V39() Element of NAT
rng a1 is Element of K19( the carrier of U0)
a1 is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0
arity a1 is V27() V28() V29() V33() V34() V39() Element of NAT
rng a1 is Element of K19( the carrier of U0)
dom a1 is functional FinSequence-membered Element of K19(( the carrier of U0 *))
K19(( the carrier of U0 *)) is non empty set
0 -tuples_on the carrier of U0 is FinSequenceSet of the carrier of U0
<*> the carrier of U0 is Relation-like NAT -defined the carrier of U0 -valued Function-like functional empty proper V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of U0
K20(NAT, the carrier of U0) is non empty V34() set
{(<*> the carrier of U0)} is non empty trivial V41(1) set
a is non empty Element of K19( the carrier of U0)
<*> a is Relation-like NAT -defined a -valued Function-like functional empty proper V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of a
K20(NAT,a) is non empty V34() set
{(<*> a)} is non empty trivial V41(1) set
0 -tuples_on a is FinSequenceSet of a
dom the charact of U0 is Element of K19(NAT)
U1 is set
the charact of U0 . U1 is set
H is V27() V28() V29() V33() V34() V39() Element of NAT
dom the charact of F is Element of K19(NAT)
the charact of F . H is set
Opers (U0,a) is Relation-like NAT -defined K36((a *),a) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36((a *),a)
a * is functional non empty FinSequence-membered FinSequenceSet of a
K36((a *),a) is set
dom (Opers (U0,a)) is Element of K19(NAT)
(Opers (U0,a)) . H is set
a1 /. a is Relation-like a * -defined a -valued Function-like non empty homogeneous V119(a) Element of K19(K20((a *),a))
K20((a *),a) is non empty set
K19(K20((a *),a)) is non empty set
H1 is Relation-like the carrier of F * -defined the carrier of F -valued Function-like non empty homogeneous V119( the carrier of F) Element of Operations F
a1 | (0 -tuples_on a) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Element of K19(K20(( the carrier of U0 *), the carrier of U0))
K20(( the carrier of U0 *), the carrier of U0) is non empty set
K19(K20(( the carrier of U0 *), the carrier of U0)) is non empty set
a is set
H1 is Element of the carrier of F
a1 is Relation-like the carrier of F * -defined the carrier of F -valued Function-like non empty homogeneous V119( the carrier of F) Element of Operations F
arity a1 is V27() V28() V29() V33() V34() V39() Element of NAT
rng a1 is Element of K19( the carrier of F)
a1 is Relation-like the carrier of F * -defined the carrier of F -valued Function-like non empty homogeneous V119( the carrier of F) Element of Operations F
arity a1 is V27() V28() V29() V33() V34() V39() Element of NAT
rng a1 is Element of K19( the carrier of F)
dom the charact of F is Element of K19(NAT)
U1 is set
the charact of F . U1 is set
H is V27() V28() V29() V33() V34() V39() Element of NAT
dom the charact of U0 is Element of K19(NAT)
the charact of U0 . H is set
signature F is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of NAT
len (signature F) is V27() V28() V29() V33() V34() V39() Element of NAT
len the charact of F is V27() V28() V29() V33() V34() V39() Element of NAT
dom (signature F) is Element of K19(NAT)
signature U0 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of NAT
H1 is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0
arity H1 is V27() V28() V29() V33() V34() V39() Element of NAT
(signature F) . H is set
dom H1 is functional FinSequence-membered Element of K19(( the carrier of U0 *))
K19(( the carrier of U0 *)) is non empty set
0 -tuples_on the carrier of U0 is FinSequenceSet of the carrier of U0
<*> the carrier of U0 is Relation-like NAT -defined the carrier of U0 -valued Function-like functional empty proper V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of U0
K20(NAT, the carrier of U0) is non empty V34() set
{(<*> the carrier of U0)} is non empty trivial V41(1) set
a is non empty Element of K19( the carrier of U0)
<*> a is Relation-like NAT -defined a -valued Function-like functional empty proper V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of a
K20(NAT,a) is non empty V34() set
{(<*> a)} is non empty trivial V41(1) set
0 -tuples_on a is FinSequenceSet of a
Opers (U0,a) is Relation-like NAT -defined K36((a *),a) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36((a *),a)
a * is functional non empty FinSequence-membered FinSequenceSet of a
K36((a *),a) is set
dom (Opers (U0,a)) is Element of K19(NAT)
(Opers (U0,a)) . H is set
H1 /. a is Relation-like a * -defined a -valued Function-like non empty homogeneous V119(a) Element of K19(K20((a *),a))
K20((a *),a) is non empty set
K19(K20((a *),a)) is non empty set
H1 | (0 -tuples_on a) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Element of K19(K20(( the carrier of U0 *), the carrier of U0))
K20(( the carrier of U0 *), the carrier of U0) is non empty set
K19(K20(( the carrier of U0 *), the carrier of U0)) is non empty set
U0 is non empty V108() V109() non-empty with_const_op UAStr
F is non empty V108() V109() non-empty SubAlgebra of U0
a is non empty V108() V109() non-empty UAStr
Constants a is Element of K19( the carrier of a)
the carrier of a is non empty set
K19( the carrier of a) is non empty set
the carrier of a * is functional non empty FinSequence-membered FinSequenceSet of the carrier of a
Operations a is non empty PFuncsDomHQN of the carrier of a
the charact of a is Relation-like NAT -defined K36(( the carrier of a *), the carrier of a) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of a *), the carrier of a)
K36(( the carrier of a *), the carrier of a) is set
rng the charact of a is set
{ b1 where b1 is Element of the carrier of a : ex b2 being Relation-like the carrier of a * -defined the carrier of a -valued Function-like non empty homogeneous V119( the carrier of a) Element of Operations a st
( arity b2 = 0 & b1 in rng b2 ) } is set
the Element of Constants a is Element of Constants a
Constants U0 is non empty Element of K19( the carrier of U0)
the carrier of U0 is non empty set
K19( the carrier of U0) is non empty set
the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0
Operations U0 is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)
K36(( the carrier of U0 *), the carrier of U0) is set
rng the charact of U0 is set
{ b1 where b1 is Element of the carrier of U0 : ex b2 being Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0 st
( arity b2 = 0 & b1 in rng b2 ) } is set
H1 is Element of the carrier of a
a1 is Relation-like the carrier of a * -defined the carrier of a -valued Function-like non empty homogeneous V119( the carrier of a) Element of Operations a
arity a1 is V27() V28() V29() V33() V34() V39() Element of NAT
rng a1 is Element of K19( the carrier of a)
U0 is non empty V108() V109() non-empty with_const_op UAStr
F is non empty V108() V109() non-empty with_const_op SubAlgebra of U0
Constants F is non empty Element of K19( the carrier of F)
the carrier of F is non empty set
K19( the carrier of F) is non empty set
the carrier of F * is functional non empty FinSequence-membered FinSequenceSet of the carrier of F
Operations F is non empty PFuncsDomHQN of the carrier of F
the charact of F is Relation-like NAT -defined K36(( the carrier of F *), the carrier of F) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of F *), the carrier of F)
K36(( the carrier of F *), the carrier of F) is set
rng the charact of F is set
{ b1 where b1 is Element of the carrier of F : ex b2 being Relation-like the carrier of F * -defined the carrier of F -valued Function-like non empty homogeneous V119( the carrier of F) Element of Operations F st
( arity b2 = 0 & b1 in rng b2 ) } is set
a is non empty V108() V109() non-empty with_const_op SubAlgebra of U0
Constants a is non empty Element of K19( the carrier of a)
the carrier of a is non empty set
K19( the carrier of a) is non empty set
the carrier of a * is functional non empty FinSequence-membered FinSequenceSet of the carrier of a
Operations a is non empty PFuncsDomHQN of the carrier of a
the charact of a is Relation-like NAT -defined K36(( the carrier of a *), the carrier of a) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of a *), the carrier of a)
K36(( the carrier of a *), the carrier of a) is set
rng the charact of a is set
{ b1 where b1 is Element of the carrier of a : ex b2 being Relation-like the carrier of a * -defined the carrier of a -valued Function-like non empty homogeneous V119( the carrier of a) Element of Operations a st
( arity b2 = 0 & b1 in rng b2 ) } is set
Constants U0 is non empty Element of K19( the carrier of U0)
the carrier of U0 is non empty set
K19( the carrier of U0) is non empty set
the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0
Operations U0 is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)
K36(( the carrier of U0 *), the carrier of U0) is set
rng the charact of U0 is set
{ b1 where b1 is Element of the carrier of U0 : ex b2 being Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0 st
( arity b2 = 0 & b1 in rng b2 ) } is set
U0 is non empty V108() V109() non-empty UAStr
(U0) is non empty (U0)
the carrier of U0 is non empty set
bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))
K19( the carrier of U0) is non empty set
K19(K19( the carrier of U0)) is non empty set
K20((U0),(bool the carrier of U0)) is non empty set
K19(K20((U0),(bool the carrier of U0))) is non empty set
(U0) is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))
F is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))
a is non empty V108() V109() non-empty (U0,(U0))
a is non empty V108() V109() non-empty SubAlgebra of U0
(U0,a) is Element of K19( the carrier of U0)
F . a is Element of bool the carrier of U0
the carrier of a is non empty set
H1 is non empty V108() V109() non-empty SubAlgebra of U0
the carrier of H1 is non empty set
a is non empty V108() V109() non-empty (U0,(U0))
F . a is Element of bool the carrier of U0
(U0,a) is Element of K19( the carrier of U0)
a is non empty V108() V109() non-empty (U0,(U0))
the carrier of a is non empty set
U0 is non empty V108() V109() non-empty UAStr
the carrier of U0 is non empty set
(U0) is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))
(U0) is non empty (U0)
bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))
K19( the carrier of U0) is non empty set
K19(K19( the carrier of U0)) is non empty set
K20((U0),(bool the carrier of U0)) is non empty set
K19(K20((U0),(bool the carrier of U0))) is non empty set
F is non empty strict V108() V109() non-empty SubAlgebra of U0
(U0) . F is set
a is Element of the carrier of U0
the carrier of F is non empty set
the carrier of F is non empty set
U0 is non empty V108() V109() non-empty UAStr
(U0) is non empty (U0)
K19((U0)) is non empty set
the carrier of U0 is non empty set
bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))
K19( the carrier of U0) is non empty set
K19(K19( the carrier of U0)) is non empty set
(U0) is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))
K20((U0),(bool the carrier of U0)) is non empty set
K19(K20((U0),(bool the carrier of U0))) is non empty set
F is non empty Element of K19((U0))
(U0) .: F is Element of K19((bool the carrier of U0))
K19((bool the carrier of U0)) is non empty set
a is non empty V108() V109() non-empty (U0,(U0))
(U0) . a is Element of bool the carrier of U0
U0 is non empty V108() V109() non-empty with_const_op UAStr
Constants U0 is non empty Element of K19( the carrier of U0)
the carrier of U0 is non empty set
K19( the carrier of U0) is non empty set
the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0
Operations U0 is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)
K36(( the carrier of U0 *), the carrier of U0) is set
rng the charact of U0 is set
{ b1 where b1 is Element of the carrier of U0 : ex b2 being Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0 st
( arity b2 = 0 & b1 in rng b2 ) } is set
(U0) is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))
(U0) is non empty (U0)
bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))
K19(K19( the carrier of U0)) is non empty set
K20((U0),(bool the carrier of U0)) is non empty set
K19(K20((U0),(bool the carrier of U0))) is non empty set
F is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
(U0) . F is set
the carrier of F is non empty set
Constants F is non empty Element of K19( the carrier of F)
K19( the carrier of F) is non empty set
the carrier of F * is functional non empty FinSequence-membered FinSequenceSet of the carrier of F
Operations F is non empty PFuncsDomHQN of the carrier of F
the charact of F is Relation-like NAT -defined K36(( the carrier of F *), the carrier of F) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of F *), the carrier of F)
K36(( the carrier of F *), the carrier of F) is set
rng the charact of F is set
{ b1 where b1 is Element of the carrier of F : ex b2 being Relation-like the carrier of F * -defined the carrier of F -valued Function-like non empty homogeneous V119( the carrier of F) Element of Operations F st
( arity b2 = 0 & b1 in rng b2 ) } is set
U0 is non empty V108() V109() non-empty with_const_op UAStr
the carrier of U0 is non empty set
Constants U0 is non empty Element of K19( the carrier of U0)
K19( the carrier of U0) is non empty set
the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0
Operations U0 is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)
K36(( the carrier of U0 *), the carrier of U0) is set
rng the charact of U0 is set
{ b1 where b1 is Element of the carrier of U0 : ex b2 being Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0 st
( arity b2 = 0 & b1 in rng b2 ) } is set
F is non empty V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of F is non empty set
a is set
K19( the carrier of F) is non empty set
U0 is non empty V108() V109() non-empty with_const_op UAStr
(U0) is non empty (U0)
K19((U0)) is non empty set
the carrier of U0 is non empty set
bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))
K19( the carrier of U0) is non empty set
K19(K19( the carrier of U0)) is non empty set
(U0) is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))
K20((U0),(bool the carrier of U0)) is non empty set
K19(K20((U0),(bool the carrier of U0))) is non empty set
F is non empty Element of K19((U0))
(U0) .: F is Element of K19((bool the carrier of U0))
K19((bool the carrier of U0)) is non empty set
meet ((U0) .: F) is Element of K19( the carrier of U0)
Constants U0 is non empty Element of K19( the carrier of U0)
the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0
Operations U0 is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)
K36(( the carrier of U0 *), the carrier of U0) is set
rng the charact of U0 is set
{ b1 where b1 is Element of the carrier of U0 : ex b2 being Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0 st
( arity b2 = 0 & b1 in rng b2 ) } is set
the Element of Constants U0 is Element of Constants U0
H1 is set
a1 is Element of K19( the carrier of U0)
U1 is non empty V108() V109() non-empty with_const_op (U0,(U0))
(U0) . U1 is Element of bool the carrier of U0
H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of H is non empty set
a is Element of K19(K19( the carrier of U0))
U0 is non empty V108() V109() non-empty with_const_op UAStr
UnSubAlLattice U0 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Sub U0 is non empty set
UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
K20((Sub U0),(Sub U0)) is non empty set
K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set
K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set
UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr
the carrier of (UnSubAlLattice U0) is non empty set
(U0) is non empty (U0)
U0 is non empty V108() V109() non-empty with_const_op UAStr
(U0) is non empty (U0)
K19((U0)) is non empty set
the carrier of U0 is non empty set
K19( the carrier of U0) is non empty set
bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))
K19(K19( the carrier of U0)) is non empty set
(U0) is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))
K20((U0),(bool the carrier of U0)) is non empty set
K19(K20((U0),(bool the carrier of U0))) is non empty set
F is non empty Element of K19((U0))
(U0) .: F is Element of K19((bool the carrier of U0))
K19((bool the carrier of U0)) is non empty set
meet ((U0) .: F) is Element of K19( the carrier of U0)
a is non empty Element of K19( the carrier of U0)
the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0
Operations U0 is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)
K36(( the carrier of U0 *), the carrier of U0) is set
rng the charact of U0 is set
a is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0
H1 is Relation-like NAT -defined a -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of a
len H1 is V27() V28() V29() V33() V34() V39() Element of NAT
arity a is V27() V28() V29() V33() V34() V39() Element of NAT
a . H1 is set
a1 is set
U1 is Element of K19( the carrier of U0)
H is non empty V108() V109() non-empty with_const_op (U0,(U0))
(U0) . H is Element of bool the carrier of U0
the carrier of H is non empty set
H1 is non empty Element of K19( the carrier of U0)
l4 is Relation-like NAT -defined H1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of H1
a . l4 is set
U0 is non empty strict V108() V109() non-empty with_const_op UAStr
(U0) is non empty (U0)
K19((U0)) is non empty set
the carrier of U0 is non empty set
bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))
K19( the carrier of U0) is non empty set
K19(K19( the carrier of U0)) is non empty set
(U0) is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))
K20((U0),(bool the carrier of U0)) is non empty set
K19(K20((U0),(bool the carrier of U0))) is non empty set
F is non empty Element of K19((U0))
(U0) .: F is Element of K19((bool the carrier of U0))
K19((bool the carrier of U0)) is non empty set
meet ((U0) .: F) is Element of K19( the carrier of U0)
a is non empty Element of K19( the carrier of U0)
UniAlgSetClosed a is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
Opers (U0,a) is Relation-like NAT -defined K36((a *),a) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36((a *),a)
a * is functional non empty FinSequence-membered FinSequenceSet of a
K36((a *),a) is set
UAStr(# a,(Opers (U0,a)) #) is strict UAStr
a is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of a is non empty set
a is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of a is non empty set
U0 is non empty V108() V109() non-empty with_const_op UAStr
UnSubAlLattice U0 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Sub U0 is non empty set
UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
K20((Sub U0),(Sub U0)) is non empty set
K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set
K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set
UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr
the carrier of (UnSubAlLattice U0) is non empty set
F is Element of the carrier of (UnSubAlLattice U0)
a is Element of the carrier of (UnSubAlLattice U0)
a is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
H1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of a is non empty set
the carrier of H1 is non empty set
a1 is Element of the carrier of (UnSubAlLattice U0)
U1 is Element of the carrier of (UnSubAlLattice U0)
the carrier of U0 is non empty set
K19( the carrier of U0) is non empty set
H1 is Element of K19( the carrier of U0)
H is Element of K19( the carrier of U0)
H1 \/ H is Element of K19( the carrier of U0)
a1 "\/" U1 is Element of the carrier of (UnSubAlLattice U0)
the L_join of (UnSubAlLattice U0) is Relation-like K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) -defined the carrier of (UnSubAlLattice U0) -valued Function-like V18(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) Element of K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)))
K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) is non empty set
K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) is non empty set
K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0))) is non empty set
K84( the carrier of (UnSubAlLattice U0), the L_join of (UnSubAlLattice U0),a1,U1) is Element of the carrier of (UnSubAlLattice U0)
a "\/" H1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
l4 is non empty Element of K19( the carrier of U0)
GenUnivAlg l4 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of a \/ the carrier of H1 is non empty set
the carrier of U0 is non empty set
K19( the carrier of U0) is non empty set
H1 is Element of K19( the carrier of U0)
H is Element of K19( the carrier of U0)
H1 \/ H is Element of K19( the carrier of U0)
l4 is non empty Element of K19( the carrier of U0)
GenUnivAlg l4 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
a "\/" H1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
a1 "\/" U1 is Element of the carrier of (UnSubAlLattice U0)
the L_join of (UnSubAlLattice U0) is Relation-like K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) -defined the carrier of (UnSubAlLattice U0) -valued Function-like V18(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) Element of K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)))
K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) is non empty set
K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) is non empty set
K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0))) is non empty set
K84( the carrier of (UnSubAlLattice U0), the L_join of (UnSubAlLattice U0),a1,U1) is Element of the carrier of (UnSubAlLattice U0)
U0 is non empty V108() V109() non-empty with_const_op UAStr
UnSubAlLattice U0 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Sub U0 is non empty set
UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
K20((Sub U0),(Sub U0)) is non empty set
K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set
K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set
UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr
the carrier of (UnSubAlLattice U0) is non empty set
F is Element of the carrier of (UnSubAlLattice U0)
a is Element of the carrier of (UnSubAlLattice U0)
a is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
H1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of a is non empty set
the carrier of H1 is non empty set
the carrier of a is non empty set
the carrier of H1 is non empty set
K19( the carrier of H1) is non empty set
U0 is non empty strict V108() V109() non-empty with_const_op UAStr
UnSubAlLattice U0 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Sub U0 is non empty set
UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
K20((Sub U0),(Sub U0)) is non empty set
K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set
K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set
UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr
the carrier of U0 is non empty set
K19( the carrier of U0) is non empty set
Constants U0 is non empty Element of K19( the carrier of U0)
the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0
Operations U0 is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)
K36(( the carrier of U0 *), the carrier of U0) is set
rng the charact of U0 is set
{ b1 where b1 is Element of the carrier of U0 : ex b2 being Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0 st
( arity b2 = 0 & b1 in rng b2 ) } is set
GenUnivAlg (Constants U0) is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of (UnSubAlLattice U0) is non empty set
a is Element of the carrier of (UnSubAlLattice U0)
H1 is Element of the carrier of (UnSubAlLattice U0)
a "/\" H1 is Element of the carrier of (UnSubAlLattice U0)
the L_meet of (UnSubAlLattice U0) is Relation-like K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) -defined the carrier of (UnSubAlLattice U0) -valued Function-like V18(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) Element of K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)))
K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) is non empty set
K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) is non empty set
K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0))) is non empty set
K84( the carrier of (UnSubAlLattice U0), the L_meet of (UnSubAlLattice U0),a,H1) is Element of the carrier of (UnSubAlLattice U0)
H1 "/\" a is Element of the carrier of (UnSubAlLattice U0)
K84( the carrier of (UnSubAlLattice U0), the L_meet of (UnSubAlLattice U0),H1,a) is Element of the carrier of (UnSubAlLattice U0)
a1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of a1 is non empty set
F is Element of K19( the carrier of U0)
U1 is Element of K19( the carrier of U0)
F \/ U1 is Element of K19( the carrier of U0)
K19( the carrier of a1) is non empty set
H is non empty Element of K19( the carrier of U0)
GenUnivAlg H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
a is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
a "\/" a1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
a "\/" H1 is Element of the carrier of (UnSubAlLattice U0)
the L_join of (UnSubAlLattice U0) is Relation-like K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) -defined the carrier of (UnSubAlLattice U0) -valued Function-like V18(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) Element of K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)))
K84( the carrier of (UnSubAlLattice U0), the L_join of (UnSubAlLattice U0),a,H1) is Element of the carrier of (UnSubAlLattice U0)
a "/\" H1 is Element of the carrier of (UnSubAlLattice U0)
H1 "/\" a is Element of the carrier of (UnSubAlLattice U0)
the carrier of (UnSubAlLattice U0) is non empty set
F is Element of the carrier of (UnSubAlLattice U0)
a is Element of the carrier of (UnSubAlLattice U0)
F "\/" a is Element of the carrier of (UnSubAlLattice U0)
the L_join of (UnSubAlLattice U0) is Relation-like K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) -defined the carrier of (UnSubAlLattice U0) -valued Function-like V18(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) Element of K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)))
K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) is non empty set
K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) is non empty set
K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0))) is non empty set
K84( the carrier of (UnSubAlLattice U0), the L_join of (UnSubAlLattice U0),F,a) is Element of the carrier of (UnSubAlLattice U0)
a "\/" F is Element of the carrier of (UnSubAlLattice U0)
K84( the carrier of (UnSubAlLattice U0), the L_join of (UnSubAlLattice U0),a,F) is Element of the carrier of (UnSubAlLattice U0)
the carrier of U0 is non empty set
K19( the carrier of U0) is non empty set
a is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of a is non empty set
H1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of H1 is non empty set
a1 is Element of K19( the carrier of U0)
U1 is Element of K19( the carrier of U0)
a1 \/ U1 is Element of K19( the carrier of U0)
H is non empty Element of K19( the carrier of U0)
F "\/" a is Element of the carrier of (UnSubAlLattice U0)
a "\/" H1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
[#] the carrier of a is non empty non proper Element of K19( the carrier of a)
K19( the carrier of a) is non empty set
GenUnivAlg ([#] the carrier of a) is non empty strict V108() V109() non-empty with_const_op SubAlgebra of a
a "\/" F is Element of the carrier of (UnSubAlLattice U0)
U0 is non empty strict V108() V109() non-empty with_const_op UAStr
UnSubAlLattice U0 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Sub U0 is non empty set
UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
K20((Sub U0),(Sub U0)) is non empty set
K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set
K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set
UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr
U0 is non empty strict V108() V109() non-empty with_const_op UAStr
Constants U0 is non empty Element of K19( the carrier of U0)
the carrier of U0 is non empty set
K19( the carrier of U0) is non empty set
the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0
Operations U0 is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)
K36(( the carrier of U0 *), the carrier of U0) is set
rng the charact of U0 is set
{ b1 where b1 is Element of the carrier of U0 : ex b2 being Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0 st
( arity b2 = 0 & b1 in rng b2 ) } is set
GenUnivAlg (Constants U0) is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
F is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
(GenUnivAlg (Constants U0)) /\ F is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of F is non empty set
K19( the carrier of F) is non empty set
the carrier of (GenUnivAlg (Constants U0)) is non empty set
the carrier of ((GenUnivAlg (Constants U0)) /\ F) is non empty set
the carrier of (GenUnivAlg (Constants U0)) /\ the carrier of F is set
U0 is non empty strict V108() V109() non-empty with_const_op UAStr
UnSubAlLattice 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
Sub U0 is non empty set
UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
K20((Sub U0),(Sub U0)) is non empty set
K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set
K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set
UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr
Bottom (UnSubAlLattice U0) is Element of the carrier of (UnSubAlLattice U0)
the carrier of (UnSubAlLattice U0) is non empty set
Constants U0 is non empty Element of K19( the carrier of U0)
the carrier of U0 is non empty set
K19( the carrier of U0) is non empty set
the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0
Operations U0 is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)
K36(( the carrier of U0 *), the carrier of U0) is set
rng the charact of U0 is set
{ b1 where b1 is Element of the carrier of U0 : ex b2 being Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0 st
( arity b2 = 0 & b1 in rng b2 ) } is set
GenUnivAlg (Constants U0) is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
(U0) is non empty (U0)
a is non empty V108() V109() non-empty with_const_op (U0,(U0))
a1 is Element of the carrier of (UnSubAlLattice U0)
U1 is non empty V108() V109() non-empty with_const_op (U0,(U0))
H1 is Element of the carrier of (UnSubAlLattice U0)
H1 "/\" a1 is Element of the carrier of (UnSubAlLattice U0)
the L_meet of (UnSubAlLattice U0) is Relation-like K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) -defined the carrier of (UnSubAlLattice U0) -valued Function-like V18(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) Element of K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)))
K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) is non empty set
K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) is non empty set
K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0))) is non empty set
K84( the carrier of (UnSubAlLattice U0), the L_meet of (UnSubAlLattice U0),H1,a1) is Element of the carrier of (UnSubAlLattice U0)
H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
(GenUnivAlg (Constants U0)) /\ H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
a1 "/\" H1 is Element of the carrier of (UnSubAlLattice U0)
K84( the carrier of (UnSubAlLattice U0), the L_meet of (UnSubAlLattice U0),a1,H1) is Element of the carrier of (UnSubAlLattice U0)
U0 is non empty strict V108() V109() non-empty with_const_op UAStr
the carrier of U0 is non empty set
K19( the carrier of U0) is non empty set
F is non empty V108() V109() non-empty with_const_op SubAlgebra of U0
a is Element of K19( the carrier of U0)
GenUnivAlg a is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
(GenUnivAlg a) "\/" F is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of F is non empty set
a \/ the carrier of F is non empty set
U0 is non empty strict V108() V109() non-empty with_const_op UAStr
the carrier of U0 is non empty set
K19( the carrier of U0) is non empty set
UnSubAlLattice 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
Sub U0 is non empty set
UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
K20((Sub U0),(Sub U0)) is non empty set
K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set
K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set
UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr
Top (UnSubAlLattice U0) is Element of the carrier of (UnSubAlLattice U0)
the carrier of (UnSubAlLattice U0) is non empty set
F is Element of K19( the carrier of U0)
GenUnivAlg F is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
(U0) is non empty (U0)
a is non empty V108() V109() non-empty with_const_op (U0,(U0))
a1 is Element of the carrier of (UnSubAlLattice U0)
U1 is non empty V108() V109() non-empty with_const_op (U0,(U0))
H1 is Element of the carrier of (UnSubAlLattice U0)
H1 "\/" a1 is Element of the carrier of (UnSubAlLattice U0)
the L_join of (UnSubAlLattice U0) is Relation-like K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) -defined the carrier of (UnSubAlLattice U0) -valued Function-like V18(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) Element of K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)))
K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) is non empty set
K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) is non empty set
K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0))) is non empty set
K84( the carrier of (UnSubAlLattice U0), the L_join of (UnSubAlLattice U0),H1,a1) is Element of the carrier of (UnSubAlLattice U0)
H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
(GenUnivAlg F) "\/" H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
a1 "\/" H1 is Element of the carrier of (UnSubAlLattice U0)
K84( the carrier of (UnSubAlLattice U0), the L_join of (UnSubAlLattice U0),a1,H1) is Element of the carrier of (UnSubAlLattice U0)
U0 is non empty strict V108() V109() non-empty with_const_op UAStr
UnSubAlLattice 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
Sub U0 is non empty set
UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
K20((Sub U0),(Sub U0)) is non empty set
K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set
K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set
UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr
Top (UnSubAlLattice U0) is Element of the carrier of (UnSubAlLattice U0)
the carrier of (UnSubAlLattice U0) is non empty set
the carrier of U0 is non empty set
K19( the carrier of U0) is non empty set
F is Element of K19( the carrier of U0)
GenUnivAlg F is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
U0 is non empty strict V108() V109() non-empty with_const_op UAStr
UnSubAlLattice 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
Sub U0 is non empty set
UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
K20((Sub U0),(Sub U0)) is non empty set
K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set
K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set
UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr
the carrier of (UnSubAlLattice U0) is non empty set
K19( the carrier of (UnSubAlLattice U0)) is non empty set
F is Element of K19( the carrier of (UnSubAlLattice U0))
Top (UnSubAlLattice U0) is Element of the carrier of (UnSubAlLattice U0)
a is Element of the carrier of (UnSubAlLattice U0)
a is Element of the carrier of (UnSubAlLattice U0)
(U0) is non empty (U0)
K19((U0)) is non empty set
a is non empty Element of K19((U0))
(U0,a) is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
a is Element of the carrier of (UnSubAlLattice U0)
the Element of a is Element of a
a1 is Element of the carrier of (UnSubAlLattice U0)
the carrier of U0 is non empty set
bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))
K19( the carrier of U0) is non empty set
K19(K19( the carrier of U0)) is non empty set
(U0) is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))
K20((U0),(bool the carrier of U0)) is non empty set
K19(K20((U0),(bool the carrier of U0))) is non empty set
H is non empty V108() V109() non-empty with_const_op (U0,(U0))
(U0) . H is Element of bool the carrier of U0
U1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of U1 is non empty set
(U0) .: a is Element of K19((bool the carrier of U0))
K19((bool the carrier of U0)) is non empty set
meet ((U0) .: a) is Element of K19( the carrier of U0)
the carrier of (U0,a) is non empty set
a1 is Element of the carrier of (UnSubAlLattice U0)
the carrier of U0 is non empty set
bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))
K19( the carrier of U0) is non empty set
K19(K19( the carrier of U0)) is non empty set
(U0) is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))
K20((U0),(bool the carrier of U0)) is non empty set
K19(K20((U0),(bool the carrier of U0))) is non empty set
(U0) .: a is Element of K19((bool the carrier of U0))
K19((bool the carrier of U0)) is non empty set
U1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of U1 is non empty set
H is set
H1 is Element of K19( the carrier of U0)
l4 is non empty V108() V109() non-empty with_const_op (U0,(U0))
(U0) . l4 is Element of bool the carrier of U0
l4 is Element of the carrier of (UnSubAlLattice U0)
U2 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of U2 is non empty set
(U0) . the Element of a is Element of bool the carrier of U0
(U0) .: F is Element of K19((bool the carrier of U0))
meet ((U0) .: a) is Element of K19( the carrier of U0)
the carrier of (U0,a) is non empty set
U0 is non empty V108() V109() non-empty with_const_op UAStr
the carrier of U0 is non empty set
F is non empty V108() V109() non-empty with_const_op UAStr
the carrier of F is non empty set
K20( the carrier of U0, the carrier of F) is non empty set
K19(K20( the carrier of U0, the carrier of F)) is non empty set
UnSubAlLattice U0 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Sub U0 is non empty set
UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
K20((Sub U0),(Sub U0)) is non empty set
K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set
K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set
UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr
the carrier of (UnSubAlLattice U0) is non empty set
UnSubAlLattice F is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Sub F is non empty set
UniAlg_join F is Relation-like K20((Sub F),(Sub F)) -defined Sub F -valued Function-like V18(K20((Sub F),(Sub F)), Sub F) Element of K19(K20(K20((Sub F),(Sub F)),(Sub F)))
K20((Sub F),(Sub F)) is non empty set
K20(K20((Sub F),(Sub F)),(Sub F)) is non empty set
K19(K20(K20((Sub F),(Sub F)),(Sub F))) is non empty set
UniAlg_meet F is Relation-like K20((Sub F),(Sub F)) -defined Sub F -valued Function-like V18(K20((Sub F),(Sub F)), Sub F) Element of K19(K20(K20((Sub F),(Sub F)),(Sub F)))
LattStr(# (Sub F),(UniAlg_join F),(UniAlg_meet F) #) is non empty strict LattStr
the carrier of (UnSubAlLattice F) is non empty set
K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice F)) is non empty set
K19(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice F))) is non empty set
K19( the carrier of F) is non empty set
a is Relation-like the carrier of U0 -defined the carrier of F -valued Function-like V18( the carrier of U0, the carrier of F) Element of K19(K20( the carrier of U0, the carrier of F))
a is set
H1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of H1 is non empty set
a .: the carrier of H1 is Element of K19( the carrier of F)
GenUnivAlg (a .: the carrier of H1) is non empty strict V108() V109() non-empty with_const_op SubAlgebra of F
a1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of F
U1 is Element of the carrier of (UnSubAlLattice F)
H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
H1 is Element of K19( the carrier of F)
the carrier of H is non empty set
a .: the carrier of H is Element of K19( the carrier of F)
GenUnivAlg (a .: the carrier of H) is non empty strict V108() V109() non-empty with_const_op SubAlgebra of F
a is Relation-like the carrier of (UnSubAlLattice U0) -defined the carrier of (UnSubAlLattice F) -valued Function-like V18( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice F)) Element of K19(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice F)))
H1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of H1 is non empty set
a .: the carrier of H1 is Element of K19( the carrier of F)
a . H1 is set
a1 is Element of K19( the carrier of F)
GenUnivAlg a1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of F
(U0) is non empty (U0)
a is Relation-like the carrier of (UnSubAlLattice U0) -defined the carrier of (UnSubAlLattice F) -valued Function-like V18( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice F)) Element of K19(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice F)))
H1 is Relation-like the carrier of (UnSubAlLattice U0) -defined the carrier of (UnSubAlLattice F) -valued Function-like V18( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice F)) Element of K19(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice F)))
a1 is set
a . a1 is set
H1 . a1 is set
U1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of U1 is non empty set
a .: the carrier of U1 is Element of K19( the carrier of F)
H is Element of K19( the carrier of F)
GenUnivAlg H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of F
U0 is non empty strict V108() V109() non-empty with_const_op UAStr
the carrier of U0 is non empty set
K20( the carrier of U0, the carrier of U0) is non empty set
K19(K20( the carrier of U0, the carrier of U0)) is non empty set
id the carrier of U0 is Relation-like non empty set
UnSubAlLattice 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
Sub U0 is non empty set
UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
K20((Sub U0),(Sub U0)) is non empty set
K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set
K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set
UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))
LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr
the carrier of (UnSubAlLattice U0) is non empty set
id the carrier of (UnSubAlLattice U0) is Relation-like non empty set
F is Relation-like the carrier of U0 -defined the carrier of U0 -valued Function-like V18( the carrier of U0, the carrier of U0) Element of K19(K20( the carrier of U0, the carrier of U0))
(U0,U0,F) is Relation-like the carrier of (UnSubAlLattice U0) -defined the carrier of (UnSubAlLattice U0) -valued Function-like V18( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) Element of K19(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)))
K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) is non empty set
K19(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0))) is non empty set
a is set
(U0,U0,F) . a is set
a is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of a is non empty set
F .: the carrier of a is Element of K19( the carrier of U0)
K19( the carrier of U0) is non empty set
H1 is set
a1 is Element of the carrier of U0
F . a1 is Element of the carrier of U0
H1 is set
a1 is Element of the carrier of U0
U1 is Element of the carrier of U0
F . U1 is Element of the carrier of U0
(U0,U0,F) . a is set
H1 is Element of K19( the carrier of U0)
GenUnivAlg H1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
dom (U0,U0,F) is Element of K19( the carrier of (UnSubAlLattice U0))
K19( the carrier of (UnSubAlLattice U0)) is non empty set