:: UNIALG_3 semantic presentation

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

len a is V27() V28() V29() V33() V34() V39() Element of NAT

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

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

K20(NAT, the carrier of U0) is non empty V34() set
{(<*> the carrier of U0)} is non empty trivial V41(1) set

K20(NAT,F) is non empty V34() set
{(<*> F)} is non empty trivial V41(1) set

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

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

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

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)

K20(NAT,a) is non empty V34() set
{(<*> a)} is non empty trivial V41(1) set

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)

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 | () 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

len () 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 () is Element of K19(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
() . 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

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)

K20(NAT,a) is non empty V34() set
{(<*> a)} is non empty trivial V41(1) 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)

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 | () 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

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),(),() #) is non empty strict LattStr
the carrier of () 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

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)

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)

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

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),(),() #) is non empty strict LattStr
the carrier of () is non empty set
F is Element of the carrier of ()
a is Element of the carrier of ()
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 ()
U1 is Element of the carrier of ()
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 ()
the L_join of () is Relation-like K20( the carrier of (), the carrier of ()) -defined the carrier of () -valued Function-like V18(K20( the carrier of (), the carrier of ()), the carrier of ()) Element of K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ()))
K20( the carrier of (), the carrier of ()) is non empty set
K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is non empty set
K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is non empty set
K84( the carrier of (), the L_join of (),a1,U1) is Element of the carrier of ()
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 ()
the L_join of () is Relation-like K20( the carrier of (), the carrier of ()) -defined the carrier of () -valued Function-like V18(K20( the carrier of (), the carrier of ()), the carrier of ()) Element of K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ()))
K20( the carrier of (), the carrier of ()) is non empty set
K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is non empty set
K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is non empty set
K84( the carrier of (), the L_join of (),a1,U1) is Element of the carrier of ()
U0 is non empty V108() V109() non-empty with_const_op UAStr

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),(),() #) is non empty strict LattStr
the carrier of () is non empty set
F is Element of the carrier of ()
a is Element of the carrier of ()
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

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),(),() #) 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 () is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
the carrier of () is non empty set
a is Element of the carrier of ()
H1 is Element of the carrier of ()
a "/\" H1 is Element of the carrier of ()
the L_meet of () is Relation-like K20( the carrier of (), the carrier of ()) -defined the carrier of () -valued Function-like V18(K20( the carrier of (), the carrier of ()), the carrier of ()) Element of K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ()))
K20( the carrier of (), the carrier of ()) is non empty set
K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is non empty set
K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is non empty set
K84( the carrier of (), the L_meet of (),a,H1) is Element of the carrier of ()
H1 "/\" a is Element of the carrier of ()
K84( the carrier of (), the L_meet of (),H1,a) is Element of the carrier of ()
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 ()
the L_join of () is Relation-like K20( the carrier of (), the carrier of ()) -defined the carrier of () -valued Function-like V18(K20( the carrier of (), the carrier of ()), the carrier of ()) Element of K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ()))
K84( the carrier of (), the L_join of (),a,H1) is Element of the carrier of ()
a "/\" H1 is Element of the carrier of ()
H1 "/\" a is Element of the carrier of ()
the carrier of () is non empty set
F is Element of the carrier of ()
a is Element of the carrier of ()
F "\/" a is Element of the carrier of ()
the L_join of () is Relation-like K20( the carrier of (), the carrier of ()) -defined the carrier of () -valued Function-like V18(K20( the carrier of (), the carrier of ()), the carrier of ()) Element of K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ()))
K20( the carrier of (), the carrier of ()) is non empty set
K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is non empty set
K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is non empty set
K84( the carrier of (), the L_join of (),F,a) is Element of the carrier of ()
a "\/" F is Element of the carrier of ()
K84( the carrier of (), the L_join of (),a,F) is Element of the carrier of ()
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 ()
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 ()
U0 is non empty strict V108() V109() non-empty with_const_op UAStr

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),(),() #) 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 () 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 ()) /\ 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 ()) is non empty set
the carrier of ((GenUnivAlg ()) /\ F) is non empty set
the carrier of (GenUnivAlg ()) /\ the carrier of F is set
U0 is non empty strict V108() V109() non-empty with_const_op UAStr

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),(),() #) is non empty strict LattStr
Bottom () is Element of the carrier of ()
the carrier of () 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 () 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 ()
U1 is non empty V108() V109() non-empty with_const_op (U0,(U0))
H1 is Element of the carrier of ()
H1 "/\" a1 is Element of the carrier of ()
the L_meet of () is Relation-like K20( the carrier of (), the carrier of ()) -defined the carrier of () -valued Function-like V18(K20( the carrier of (), the carrier of ()), the carrier of ()) Element of K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ()))
K20( the carrier of (), the carrier of ()) is non empty set
K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is non empty set
K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is non empty set
K84( the carrier of (), the L_meet of (),H1,a1) is Element of the carrier of ()
H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
(GenUnivAlg ()) /\ H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
a1 "/\" H1 is Element of the carrier of ()
K84( the carrier of (), the L_meet of (),a1,H1) is Element of the carrier of ()
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
() "\/" 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

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),(),() #) is non empty strict LattStr
Top () is Element of the carrier of ()
the carrier of () 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 ()
U1 is non empty V108() V109() non-empty with_const_op (U0,(U0))
H1 is Element of the carrier of ()
H1 "\/" a1 is Element of the carrier of ()
the L_join of () is Relation-like K20( the carrier of (), the carrier of ()) -defined the carrier of () -valued Function-like V18(K20( the carrier of (), the carrier of ()), the carrier of ()) Element of K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ()))
K20( the carrier of (), the carrier of ()) is non empty set
K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is non empty set
K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is non empty set
K84( the carrier of (), the L_join of (),H1,a1) is Element of the carrier of ()
H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
() "\/" H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0
a1 "\/" H1 is Element of the carrier of ()
K84( the carrier of (), the L_join of (),a1,H1) is Element of the carrier of ()
U0 is non empty strict V108() V109() non-empty with_const_op UAStr

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),(),() #) is non empty strict LattStr
Top () is Element of the carrier of ()
the carrier of () 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

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),(),() #) is non empty strict LattStr
the carrier of () is non empty set
K19( the carrier of ()) is non empty set
F is Element of K19( the carrier of ())
Top () is Element of the carrier of ()
a is Element of the carrier of ()
a is Element of the carrier of ()
(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 ()
the Element of a is Element of a
a1 is Element of the carrier of ()
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 ()
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 ()
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

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),(),() #) is non empty strict LattStr
the carrier of () is non empty set

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),(),() #) is non empty strict LattStr
the carrier of () is non empty set
K20( the carrier of (), the carrier of ()) is non empty set
K19(K20( the carrier of (), the carrier of ())) 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 ()
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 () -defined the carrier of () -valued Function-like V18( the carrier of (), the carrier of ()) Element of K19(K20( the carrier of (), the carrier of ()))
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 () -defined the carrier of () -valued Function-like V18( the carrier of (), the carrier of ()) Element of K19(K20( the carrier of (), the carrier of ()))
H1 is Relation-like the carrier of () -defined the carrier of () -valued Function-like V18( the carrier of (), the carrier of ()) Element of K19(K20( the carrier of (), the carrier of ()))
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

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),(),() #) is non empty strict LattStr
the carrier of () is non empty set
id the carrier of () 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 () -defined the carrier of () -valued Function-like V18( the carrier of (), the carrier of ()) Element of K19(K20( the carrier of (), the carrier of ()))
K20( the carrier of (), the carrier of ()) is non empty set
K19(K20( the carrier of (), the carrier of ())) 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 ())
K19( the carrier of ()) is non empty set