:: LATTICE2 semantic presentation

K142() is set
K19(K142()) is set
K146() is Element of K19(K142())
K141() is set
K19(K141()) is set
{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
1 is non empty set
L is set
K19(L) is set
L is non empty set
K20(L,L) is Relation-like set
K19(K20(L,L)) is set
C is Element of K19(L)
p is Relation-like L -defined L -valued Function-like V14(L) V18(L,L) Element of K19(K20(L,L))
p | C is Relation-like L -defined C -defined L -defined L -valued Function-like Element of K19(K20(L,L))
dom (p | C) is set
dom p is set
(dom p) /\ C is Element of K19(L)
L /\ C is Element of K19(L)
L is set
K19(L) is set
L is non empty set
K20(L,L) is Relation-like set
K19(K20(L,L)) is set
C is Element of K19(L)
p is Relation-like L -defined L -valued Function-like V14(L) V18(L,L) Element of K19(K20(L,L))
p | C is Relation-like L -defined C -defined L -defined L -valued Function-like Element of K19(K20(L,L))
q is Relation-like L -defined L -valued Function-like V14(L) V18(L,L) Element of K19(K20(L,L))
q | C is Relation-like L -defined C -defined L -defined L -valued Function-like Element of K19(K20(L,L))
B is Element of L
q . B is set
p . B is set
(q | C) . B is set
K20(C,L) is Relation-like set
K19(K20(C,L)) is set
r is set
B is Relation-like C -defined L -valued Function-like V14(C) V18(C,L) Element of K19(K20(C,L))
B . r is set
p . r is set
q . r is set
B is Relation-like C -defined L -valued Function-like V14(C) V18(C,L) Element of K19(K20(C,L))
B . r is set
B | C is Relation-like C -defined C -defined L -valued Function-like Element of K19(K20(C,L))
B | C is Relation-like C -defined C -defined L -valued Function-like Element of K19(K20(C,L))
L is set
L is non empty set
K20(L,L) is Relation-like set
K19(K20(L,L)) is set
C is Relation-like L -defined L -valued Function-like V14(L) V18(L,L) Element of K19(K20(L,L))
p is Relation-like L -defined L -valued Function-like V14(L) V18(L,L) Element of K19(K20(L,L))
q is set
p | q is Relation-like L -defined q -defined L -defined L -valued Function-like Element of K19(K20(L,L))
C +* (p | q) is Relation-like L -defined L -valued Function-like Element of K19(K20(L,L))
dom C is set
dom p is set
dom (C +* (p | q)) is set
dom (p | q) is set
(dom C) \/ (dom (p | q)) is set
(dom p) /\ q is set
(dom C) \/ ((dom p) /\ q) is set
L is set
K19(L) is set
L is non empty set
K20(L,L) is Relation-like set
K19(K20(L,L)) is set
C is Element of K19(L)
p is Relation-like L -defined L -valued Function-like V14(L) V18(L,L) Element of K19(K20(L,L))
p | C is Relation-like L -defined C -defined L -defined L -valued Function-like Element of K19(K20(L,L))
q is Relation-like L -defined L -valued Function-like V14(L) V18(L,L) Element of K19(K20(L,L))
(p | C) +* q is Relation-like L -defined L -valued Function-like Element of K19(K20(L,L))
dom (p | C) is set
dom q is set
L is Relation-like Function-like set
L is Relation-like Function-like set
L +* L is Relation-like Function-like set
dom L is set
dom L is set
(dom L) \/ (dom L) is set
C is set
L . C is set
L . C is set
L is set
K19(L) is set
L is non empty set
K20(L,L) is Relation-like set
K19(K20(L,L)) is set
p is Relation-like L -defined L -valued Function-like V14(L) V18(L,L) Element of K19(K20(L,L))
C is Element of K19(L)
p | C is Relation-like L -defined C -defined L -defined L -valued Function-like Element of K19(K20(L,L))
p +* (p | C) is Relation-like L -defined L -valued Function-like Element of K19(K20(L,L))
L is set
K19(L) is set
L is non empty set
K20(L,L) is Relation-like set
K19(K20(L,L)) is set
C is Element of K19(L)
p is Relation-like L -defined L -valued Function-like V14(L) V18(L,L) Element of K19(K20(L,L))
p | C is Relation-like L -defined C -defined L -defined L -valued Function-like Element of K19(K20(L,L))
q is Relation-like L -defined L -valued Function-like V14(L) V18(L,L) Element of K19(K20(L,L))
q +* (p | C) is Relation-like L -defined L -valued Function-like Element of K19(K20(L,L))
q | C is Relation-like L -defined C -defined L -defined L -valued Function-like Element of K19(K20(L,L))
L is set
Fin L is preBoolean set
L is non empty set
K20(L,L) is Relation-like set
K19(K20(L,L)) is set
C is Relation-like L -defined L -valued Function-like V14(L) V18(L,L) Element of K19(K20(L,L))
p is Relation-like L -defined L -valued Function-like V14(L) V18(L,L) Element of K19(K20(L,L))
q is Element of Fin L
C | q is Relation-like L -defined q -defined L -defined L -valued Function-like Element of K19(K20(L,L))
(C | q) +* p is Relation-like L -defined L -valued Function-like Element of K19(K20(L,L))
K19(L) is set
B is Element of K19(L)
C | B is Relation-like L -defined B -defined L -defined L -valued Function-like Element of K19(K20(L,L))
(C | B) +* p is Relation-like L -defined L -valued Function-like Element of K19(K20(L,L))
L is set
Fin L is preBoolean set
L is non empty set
K20(L,L) is Relation-like set
K19(K20(L,L)) is set
C is Relation-like L -defined L -valued Function-like V14(L) V18(L,L) Element of K19(K20(L,L))
p is Element of Fin L
C | p is Relation-like L -defined p -defined L -defined L -valued Function-like Element of K19(K20(L,L))
dom (C | p) is set
K19(L) is set
q is Element of K19(L)
C | q is Relation-like L -defined q -defined L -defined L -valued Function-like Element of K19(K20(L,L))
dom (C | q) is set
L is set
Fin L is preBoolean set
L is non empty set
K20(L,L) is Relation-like set
K19(K20(L,L)) is set
C is Relation-like L -defined L -valued Function-like V14(L) V18(L,L) Element of K19(K20(L,L))
p is Relation-like L -defined L -valued Function-like V14(L) V18(L,L) Element of K19(K20(L,L))
q is Element of Fin L
C | q is Relation-like L -defined q -defined L -defined L -valued Function-like Element of K19(K20(L,L))
p +* (C | q) is Relation-like L -defined L -valued Function-like Element of K19(K20(L,L))
K19(L) is set
B is Element of K19(L)
C | B is Relation-like L -defined B -defined L -defined L -valued Function-like Element of K19(K20(L,L))
p +* (C | B) is Relation-like L -defined L -valued Function-like Element of K19(K20(L,L))
B is Element of L
C . B is set
p . B is set
L is non empty set
K20(L,L) is Relation-like set
K20(K20(L,L),L) is Relation-like set
K19(K20(K20(L,L),L)) is set
L is non empty set
K20(L,L) is Relation-like set
K20(K20(L,L),L) is Relation-like set
K19(K20(K20(L,L),L)) is set
L is non empty LattStr
the carrier of L is non empty set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
L is Element of the carrier of L
C is Element of the carrier of L
L "\/" C is Element of the carrier of L
the L_join of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_join of L . [L,C] is set
C "\/" L is Element of the carrier of L
the L_join of L . (C,L) is Element of the carrier of L
[C,L] is set
the L_join of L . [C,L] is set
L is Element of the carrier of L
C is Element of the carrier of L
p is Element of the carrier of L
C "\/" p is Element of the carrier of L
the L_join of L . (C,p) is Element of the carrier of L
[C,p] is set
the L_join of L . [C,p] is set
L "\/" (C "\/" p) is Element of the carrier of L
the L_join of L . (L,(C "\/" p)) is Element of the carrier of L
[L,(C "\/" p)] is set
the L_join of L . [L,(C "\/" p)] is set
L "\/" C is Element of the carrier of L
the L_join of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_join of L . [L,C] is set
(L "\/" C) "\/" p is Element of the carrier of L
the L_join of L . ((L "\/" C),p) is Element of the carrier of L
[(L "\/" C),p] is set
the L_join of L . [(L "\/" C),p] is set
L is Element of the carrier of L
C is Element of the carrier of L
L "/\" C is Element of the carrier of L
the L_meet of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_meet of L . [L,C] is set
(L "/\" C) "\/" C is Element of the carrier of L
the L_join of L . ((L "/\" C),C) is Element of the carrier of L
[(L "/\" C),C] is set
the L_join of L . [(L "/\" C),C] is set
C "\/" (L "/\" C) is Element of the carrier of L
the L_join of L . (C,(L "/\" C)) is Element of the carrier of L
[C,(L "/\" C)] is set
the L_join of L . [C,(L "/\" C)] is set
C "/\" L is Element of the carrier of L
the L_meet of L . (C,L) is Element of the carrier of L
[C,L] is set
the L_meet of L . [C,L] is set
C "\/" (C "/\" L) is Element of the carrier of L
the L_join of L . (C,(C "/\" L)) is Element of the carrier of L
[C,(C "/\" L)] is set
the L_join of L . [C,(C "/\" L)] is set
L is Element of the carrier of L
C is Element of the carrier of L
L "/\" C is Element of the carrier of L
the L_meet of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_meet of L . [L,C] is set
C "/\" L is Element of the carrier of L
the L_meet of L . (C,L) is Element of the carrier of L
[C,L] is set
the L_meet of L . [C,L] is set
L is Element of the carrier of L
C is Element of the carrier of L
p is Element of the carrier of L
C "/\" p is Element of the carrier of L
the L_meet of L . (C,p) is Element of the carrier of L
[C,p] is set
the L_meet of L . [C,p] is set
L "/\" (C "/\" p) is Element of the carrier of L
the L_meet of L . (L,(C "/\" p)) is Element of the carrier of L
[L,(C "/\" p)] is set
the L_meet of L . [L,(C "/\" p)] is set
L "/\" C is Element of the carrier of L
the L_meet of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_meet of L . [L,C] is set
(L "/\" C) "/\" p is Element of the carrier of L
the L_meet of L . ((L "/\" C),p) is Element of the carrier of L
[(L "/\" C),p] is set
the L_meet of L . [(L "/\" C),p] is set
L is Element of the carrier of L
C is Element of the carrier of L
L "\/" C is Element of the carrier of L
the L_join of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_join of L . [L,C] is set
L "/\" (L "\/" C) is Element of the carrier of L
the L_meet of L . (L,(L "\/" C)) is Element of the carrier of L
[L,(L "\/" C)] is set
the L_meet of L . [L,(L "\/" C)] is set
L is LattStr
the carrier of L is set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is strict LattStr
L is non empty LattStr
(L) is strict LattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
L is non empty LattStr
the carrier of L is non empty set
(L) is non empty strict LattStr
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
the carrier of (L) is non empty set
L is non empty LattStr
the carrier of L is non empty set
K20( the carrier of L, the carrier of L) is Relation-like set
(L) is non empty strict LattStr
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
the carrier of (L) is non empty set
K20( the carrier of (L), the carrier of (L)) is Relation-like set
the L_meet of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) is Relation-like set
K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L))) is set
C is non empty LattStr
the carrier of C is non empty set
K20( the carrier of C, the carrier of C) is Relation-like set
(C) is non empty strict LattStr
the L_meet of C is Relation-like K20( the carrier of C, the carrier of C) -defined the carrier of C -valued Function-like V14(K20( the carrier of C, the carrier of C)) V18(K20( the carrier of C, the carrier of C), the carrier of C) Element of K19(K20(K20( the carrier of C, the carrier of C), the carrier of C))
K20(K20( the carrier of C, the carrier of C), the carrier of C) is Relation-like set
K19(K20(K20( the carrier of C, the carrier of C), the carrier of C)) is set
the L_join of C is Relation-like K20( the carrier of C, the carrier of C) -defined the carrier of C -valued Function-like V14(K20( the carrier of C, the carrier of C)) V18(K20( the carrier of C, the carrier of C), the carrier of C) Element of K19(K20(K20( the carrier of C, the carrier of C), the carrier of C))
LattStr(# the carrier of C, the L_meet of C, the L_join of C #) is non empty strict LattStr
the carrier of (C) is non empty set
K20( the carrier of (C), the carrier of (C)) is Relation-like set
the L_join of (C) is Relation-like K20( the carrier of (C), the carrier of (C)) -defined the carrier of (C) -valued Function-like V14(K20( the carrier of (C), the carrier of (C))) V18(K20( the carrier of (C), the carrier of (C)), the carrier of (C)) Element of K19(K20(K20( the carrier of (C), the carrier of (C)), the carrier of (C)))
K20(K20( the carrier of (C), the carrier of (C)), the carrier of (C)) is Relation-like set
K19(K20(K20( the carrier of (C), the carrier of (C)), the carrier of (C))) is set
L is non empty strict LattStr
(L) is non empty strict LattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
((L)) is non empty strict LattStr
the carrier of (L) is non empty set
the L_meet of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
K20( the carrier of (L), the carrier of (L)) is Relation-like set
K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) is Relation-like set
K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L))) is set
the L_join of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
LattStr(# the carrier of (L), the L_meet of (L), the L_join of (L) #) is non empty strict LattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
Bottom L is Element of the carrier of L
L is Element of the carrier of L
C is Element of the carrier of L
C "\/" L is Element of the carrier of L
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . (C,L) is Element of the carrier of L
[C,L] is set
the L_join of L . [C,L] is set
C "/\" L is Element of the carrier of L
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
the L_meet of L . (C,L) is Element of the carrier of L
the L_meet of L . [C,L] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
Bottom L is Element of the carrier of L
L is Element of the carrier of L
C is Element of the carrier of L
L "\/" C is Element of the carrier of L
the L_join of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_join of L . [L,C] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
Top L is Element of the carrier of L
L is Element of the carrier of L
C is Element of the carrier of L
C "/\" L is Element of the carrier of L
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . (C,L) is Element of the carrier of L
[C,L] is set
the L_meet of L . [C,L] is set
C "\/" L is Element of the carrier of L
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
the L_join of L . (C,L) is Element of the carrier of L
the L_join of L . [C,L] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
Top L is Element of the carrier of L
L is Element of the carrier of L
C is Element of the carrier of L
L "/\" C is Element of the carrier of L
the L_meet of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_meet of L . [L,C] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
L is Element of the carrier of L
the L_join of L . (L,L) is Element of the carrier of L
[L,L] is set
the L_join of L . [L,L] is set
the L_join of L . (L,L) is Element of the carrier of L
L "\/" L is Element of the carrier of L
L is non empty join-commutative \/-SemiLattStr
the carrier of L is non empty set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
L is Element of the carrier of L
C is Element of the carrier of L
the L_join of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_join of L . [L,C] is set
the L_join of L . (C,L) is Element of the carrier of L
[C,L] is set
the L_join of L . [C,L] is set
the L_join of L . (L,C) is Element of the carrier of L
C "\/" L is Element of the carrier of L
the L_join of L . (C,L) is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
Bottom L is Element of the carrier of L
the_unity_wrt the L_join of L is Element of the carrier of L
C is Element of the carrier of L
p is Element of the carrier of L
the L_join of L . (C,p) is Element of the carrier of L
[C,p] is set
the L_join of L . [C,p] is set
L is non empty join-associative \/-SemiLattStr
the carrier of L is non empty set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
L is Element of the carrier of L
C is Element of the carrier of L
p is Element of the carrier of L
the L_join of L . (C,p) is Element of the carrier of L
[C,p] is set
the L_join of L . [C,p] is set
the L_join of L . (L,( the L_join of L . (C,p))) is Element of the carrier of L
[L,( the L_join of L . (C,p))] is set
the L_join of L . [L,( the L_join of L . (C,p))] is set
the L_join of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_join of L . [L,C] is set
the L_join of L . (( the L_join of L . (L,C)),p) is Element of the carrier of L
[( the L_join of L . (L,C)),p] is set
the L_join of L . [( the L_join of L . (L,C)),p] is set
the L_join of L . (C,p) is Element of the carrier of L
the L_join of L . (L,( the L_join of L . (C,p))) is Element of the carrier of L
[L,( the L_join of L . (C,p))] is set
the L_join of L . [L,( the L_join of L . (C,p))] is set
C "\/" p is Element of the carrier of L
L "\/" (C "\/" p) is Element of the carrier of L
the L_join of L . (L,(C "\/" p)) is Element of the carrier of L
[L,(C "\/" p)] is set
the L_join of L . [L,(C "\/" p)] is set
L "\/" C is Element of the carrier of L
the L_join of L . (L,C) is Element of the carrier of L
(L "\/" C) "\/" p is Element of the carrier of L
the L_join of L . ((L "\/" C),p) is Element of the carrier of L
[(L "\/" C),p] is set
the L_join of L . [(L "\/" C),p] is set
the L_join of L . (( the L_join of L . (L,C)),p) is Element of the carrier of L
[( the L_join of L . (L,C)),p] is set
the L_join of L . [( the L_join of L . (L,C)),p] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
L is Element of the carrier of L
the L_meet of L . (L,L) is Element of the carrier of L
[L,L] is set
the L_meet of L . [L,L] is set
the L_meet of L . (L,L) is Element of the carrier of L
L "/\" L is Element of the carrier of L
L is non empty meet-commutative /\-SemiLattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
L is Element of the carrier of L
C is Element of the carrier of L
the L_meet of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_meet of L . [L,C] is set
the L_meet of L . (C,L) is Element of the carrier of L
[C,L] is set
the L_meet of L . [C,L] is set
the L_meet of L . (L,C) is Element of the carrier of L
C "/\" L is Element of the carrier of L
the L_meet of L . (C,L) is Element of the carrier of L
L is non empty meet-associative /\-SemiLattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
L is Element of the carrier of L
C is Element of the carrier of L
p is Element of the carrier of L
the L_meet of L . (C,p) is Element of the carrier of L
[C,p] is set
the L_meet of L . [C,p] is set
the L_meet of L . (L,( the L_meet of L . (C,p))) is Element of the carrier of L
[L,( the L_meet of L . (C,p))] is set
the L_meet of L . [L,( the L_meet of L . (C,p))] is set
the L_meet of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_meet of L . [L,C] is set
the L_meet of L . (( the L_meet of L . (L,C)),p) is Element of the carrier of L
[( the L_meet of L . (L,C)),p] is set
the L_meet of L . [( the L_meet of L . (L,C)),p] is set
the L_meet of L . (C,p) is Element of the carrier of L
the L_meet of L . (L,( the L_meet of L . (C,p))) is Element of the carrier of L
[L,( the L_meet of L . (C,p))] is set
the L_meet of L . [L,( the L_meet of L . (C,p))] is set
C "/\" p is Element of the carrier of L
L "/\" (C "/\" p) is Element of the carrier of L
the L_meet of L . (L,(C "/\" p)) is Element of the carrier of L
[L,(C "/\" p)] is set
the L_meet of L . [L,(C "/\" p)] is set
L "/\" C is Element of the carrier of L
the L_meet of L . (L,C) is Element of the carrier of L
(L "/\" C) "/\" p is Element of the carrier of L
the L_meet of L . ((L "/\" C),p) is Element of the carrier of L
[(L "/\" C),p] is set
the L_meet of L . [(L "/\" C),p] is set
the L_meet of L . (( the L_meet of L . (L,C)),p) is Element of the carrier of L
[( the L_meet of L . (L,C)),p] is set
the L_meet of L . [( the L_meet of L . (L,C)),p] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
Top L is Element of the carrier of L
the_unity_wrt the L_meet of L is Element of the carrier of L
C is Element of the carrier of L
p is Element of the carrier of L
the L_meet of L . (C,p) is Element of the carrier of L
[C,p] is set
the L_meet of L . [C,p] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
L is Element of the carrier of L
C is Element of the carrier of L
p is Element of the carrier of L
the L_join of L . (C,p) is Element of the carrier of L
[C,p] is set
the L_join of L . [C,p] is set
the L_join of L . (L,( the L_join of L . (C,p))) is Element of the carrier of L
[L,( the L_join of L . (C,p))] is set
the L_join of L . [L,( the L_join of L . (C,p))] is set
C "\/" p is Element of the carrier of L
L "\/" (C "\/" p) is Element of the carrier of L
the L_join of L . (L,(C "\/" p)) is Element of the carrier of L
[L,(C "\/" p)] is set
the L_join of L . [L,(C "\/" p)] is set
L "\/" C is Element of the carrier of L
the L_join of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_join of L . [L,C] is set
(L "\/" C) "\/" p is Element of the carrier of L
the L_join of L . ((L "\/" C),p) is Element of the carrier of L
[(L "\/" C),p] is set
the L_join of L . [(L "\/" C),p] is set
L "\/" L is Element of the carrier of L
the L_join of L . (L,L) is Element of the carrier of L
[L,L] is set
the L_join of L . [L,L] is set
(L "\/" L) "\/" C is Element of the carrier of L
the L_join of L . ((L "\/" L),C) is Element of the carrier of L
[(L "\/" L),C] is set
the L_join of L . [(L "\/" L),C] is set
((L "\/" L) "\/" C) "\/" p is Element of the carrier of L
the L_join of L . (((L "\/" L) "\/" C),p) is Element of the carrier of L
[((L "\/" L) "\/" C),p] is set
the L_join of L . [((L "\/" L) "\/" C),p] is set
(L "\/" C) "\/" L is Element of the carrier of L
the L_join of L . ((L "\/" C),L) is Element of the carrier of L
[(L "\/" C),L] is set
the L_join of L . [(L "\/" C),L] is set
((L "\/" C) "\/" L) "\/" p is Element of the carrier of L
the L_join of L . (((L "\/" C) "\/" L),p) is Element of the carrier of L
[((L "\/" C) "\/" L),p] is set
the L_join of L . [((L "\/" C) "\/" L),p] is set
L "\/" p is Element of the carrier of L
the L_join of L . (L,p) is Element of the carrier of L
[L,p] is set
the L_join of L . [L,p] is set
(L "\/" C) "\/" (L "\/" p) is Element of the carrier of L
the L_join of L . ((L "\/" C),(L "\/" p)) is Element of the carrier of L
[(L "\/" C),(L "\/" p)] is set
the L_join of L . [(L "\/" C),(L "\/" p)] is set
the L_join of L . (( the L_join of L . (L,C)),( the L_join of L . (L,p))) is Element of the carrier of L
[( the L_join of L . (L,C)),( the L_join of L . (L,p))] is set
the L_join of L . [( the L_join of L . (L,C)),( the L_join of L . (L,p))] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
L is Element of the carrier of L
C is Element of the carrier of L
p is Element of the carrier of L
the L_meet of L . (C,p) is Element of the carrier of L
[C,p] is set
the L_meet of L . [C,p] is set
the L_join of L . (L,( the L_meet of L . (C,p))) is Element of the carrier of L
[L,( the L_meet of L . (C,p))] is set
the L_join of L . [L,( the L_meet of L . (C,p))] is set
C "/\" p is Element of the carrier of L
L "\/" (C "/\" p) is Element of the carrier of L
the L_join of L . (L,(C "/\" p)) is Element of the carrier of L
[L,(C "/\" p)] is set
the L_join of L . [L,(C "/\" p)] is set
L "\/" C is Element of the carrier of L
the L_join of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_join of L . [L,C] is set
L "\/" p is Element of the carrier of L
the L_join of L . (L,p) is Element of the carrier of L
[L,p] is set
the L_join of L . [L,p] is set
(L "\/" C) "/\" (L "\/" p) is Element of the carrier of L
the L_meet of L . ((L "\/" C),(L "\/" p)) is Element of the carrier of L
[(L "\/" C),(L "\/" p)] is set
the L_meet of L . [(L "\/" C),(L "\/" p)] is set
the L_meet of L . (( the L_join of L . (L,C)),( the L_join of L . (L,p))) is Element of the carrier of L
[( the L_join of L . (L,C)),( the L_join of L . (L,p))] is set
the L_meet of L . [( the L_join of L . (L,C)),( the L_join of L . (L,p))] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
L is Element of the carrier of L
C is Element of the carrier of L
p is Element of the carrier of L
C "/\" p is Element of the carrier of L
the L_meet of L . (C,p) is Element of the carrier of L
[C,p] is set
the L_meet of L . [C,p] is set
L "\/" (C "/\" p) is Element of the carrier of L
the L_join of L . (L,(C "/\" p)) is Element of the carrier of L
[L,(C "/\" p)] is set
the L_join of L . [L,(C "/\" p)] is set
L "\/" C is Element of the carrier of L
the L_join of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_join of L . [L,C] is set
L "\/" p is Element of the carrier of L
the L_join of L . (L,p) is Element of the carrier of L
[L,p] is set
the L_join of L . [L,p] is set
(L "\/" C) "/\" (L "\/" p) is Element of the carrier of L
the L_meet of L . ((L "\/" C),(L "\/" p)) is Element of the carrier of L
[(L "\/" C),(L "\/" p)] is set
the L_meet of L . [(L "\/" C),(L "\/" p)] is set
L is Element of the carrier of L
C is Element of the carrier of L
L "/\" C is Element of the carrier of L
the L_meet of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_meet of L . [L,C] is set
p is Element of the carrier of L
C "\/" p is Element of the carrier of L
the L_join of L . (C,p) is Element of the carrier of L
[C,p] is set
the L_join of L . [C,p] is set
L "/\" (C "\/" p) is Element of the carrier of L
the L_meet of L . (L,(C "\/" p)) is Element of the carrier of L
[L,(C "\/" p)] is set
the L_meet of L . [L,(C "\/" p)] is set
L "/\" p is Element of the carrier of L
the L_meet of L . (L,p) is Element of the carrier of L
[L,p] is set
the L_meet of L . [L,p] is set
(L "/\" C) "\/" (L "/\" p) is Element of the carrier of L
the L_join of L . ((L "/\" C),(L "/\" p)) is Element of the carrier of L
[(L "/\" C),(L "/\" p)] is set
the L_join of L . [(L "/\" C),(L "/\" p)] is set
C "\/" p is Element of the carrier of L
L "/\" (C "\/" p) is Element of the carrier of L
the L_meet of L . (L,(C "\/" p)) is Element of the carrier of L
[L,(C "\/" p)] is set
the L_meet of L . [L,(C "\/" p)] is set
p "\/" L is Element of the carrier of L
the L_join of L . (p,L) is Element of the carrier of L
[p,L] is set
the L_join of L . [p,L] is set
L "/\" (p "\/" L) is Element of the carrier of L
the L_meet of L . (L,(p "\/" L)) is Element of the carrier of L
[L,(p "\/" L)] is set
the L_meet of L . [L,(p "\/" L)] is set
p "\/" C is Element of the carrier of L
the L_join of L . (p,C) is Element of the carrier of L
[p,C] is set
the L_join of L . [p,C] is set
(L "/\" (p "\/" L)) "/\" (p "\/" C) is Element of the carrier of L
the L_meet of L . ((L "/\" (p "\/" L)),(p "\/" C)) is Element of the carrier of L
[(L "/\" (p "\/" L)),(p "\/" C)] is set
the L_meet of L . [(L "/\" (p "\/" L)),(p "\/" C)] is set
(p "\/" L) "/\" (p "\/" C) is Element of the carrier of L
the L_meet of L . ((p "\/" L),(p "\/" C)) is Element of the carrier of L
[(p "\/" L),(p "\/" C)] is set
the L_meet of L . [(p "\/" L),(p "\/" C)] is set
L "/\" ((p "\/" L) "/\" (p "\/" C)) is Element of the carrier of L
the L_meet of L . (L,((p "\/" L) "/\" (p "\/" C))) is Element of the carrier of L
[L,((p "\/" L) "/\" (p "\/" C))] is set
the L_meet of L . [L,((p "\/" L) "/\" (p "\/" C))] is set
L "/\" C is Element of the carrier of L
(L "/\" C) "\/" p is Element of the carrier of L
the L_join of L . ((L "/\" C),p) is Element of the carrier of L
[(L "/\" C),p] is set
the L_join of L . [(L "/\" C),p] is set
L "/\" ((L "/\" C) "\/" p) is Element of the carrier of L
the L_meet of L . (L,((L "/\" C) "\/" p)) is Element of the carrier of L
[L,((L "/\" C) "\/" p)] is set
the L_meet of L . [L,((L "/\" C) "\/" p)] is set
(L "/\" C) "\/" L is Element of the carrier of L
the L_join of L . ((L "/\" C),L) is Element of the carrier of L
[(L "/\" C),L] is set
the L_join of L . [(L "/\" C),L] is set
((L "/\" C) "\/" L) "/\" ((L "/\" C) "\/" p) is Element of the carrier of L
the L_meet of L . (((L "/\" C) "\/" L),((L "/\" C) "\/" p)) is Element of the carrier of L
[((L "/\" C) "\/" L),((L "/\" C) "\/" p)] is set
the L_meet of L . [((L "/\" C) "\/" L),((L "/\" C) "\/" p)] is set
L "/\" p is Element of the carrier of L
(L "/\" C) "\/" (L "/\" p) is Element of the carrier of L
the L_join of L . ((L "/\" C),(L "/\" p)) is Element of the carrier of L
[(L "/\" C),(L "/\" p)] is set
the L_join of L . [(L "/\" C),(L "/\" p)] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
L is Element of the carrier of L
C is Element of the carrier of L
p is Element of the carrier of L
the L_join of L . (C,p) is Element of the carrier of L
[C,p] is set
the L_join of L . [C,p] is set
the L_meet of L . (L,( the L_join of L . (C,p))) is Element of the carrier of L
[L,( the L_join of L . (C,p))] is set
the L_meet of L . [L,( the L_join of L . (C,p))] is set
C "\/" p is Element of the carrier of L
L "/\" (C "\/" p) is Element of the carrier of L
the L_meet of L . (L,(C "\/" p)) is Element of the carrier of L
[L,(C "\/" p)] is set
the L_meet of L . [L,(C "\/" p)] is set
L "/\" C is Element of the carrier of L
the L_meet of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_meet of L . [L,C] is set
L "/\" p is Element of the carrier of L
the L_meet of L . (L,p) is Element of the carrier of L
[L,p] is set
the L_meet of L . [L,p] is set
(L "/\" C) "\/" (L "/\" p) is Element of the carrier of L
the L_join of L . ((L "/\" C),(L "/\" p)) is Element of the carrier of L
[(L "/\" C),(L "/\" p)] is set
the L_join of L . [(L "/\" C),(L "/\" p)] is set
the L_join of L . (( the L_meet of L . (L,C)),( the L_meet of L . (L,p))) is Element of the carrier of L
[( the L_meet of L . (L,C)),( the L_meet of L . (L,p))] is set
the L_join of L . [( the L_meet of L . (L,C)),( the L_meet of L . (L,p))] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
L is Element of the carrier of L
C is Element of the carrier of L
L "/\" C is Element of the carrier of L
the L_meet of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_meet of L . [L,C] is set
p is Element of the carrier of L
C "\/" p is Element of the carrier of L
the L_join of L . (C,p) is Element of the carrier of L
[C,p] is set
the L_join of L . [C,p] is set
L "/\" (C "\/" p) is Element of the carrier of L
the L_meet of L . (L,(C "\/" p)) is Element of the carrier of L
[L,(C "\/" p)] is set
the L_meet of L . [L,(C "\/" p)] is set
L "/\" p is Element of the carrier of L
the L_meet of L . (L,p) is Element of the carrier of L
[L,p] is set
the L_meet of L . [L,p] is set
(L "/\" C) "\/" (L "/\" p) is Element of the carrier of L
the L_join of L . ((L "/\" C),(L "/\" p)) is Element of the carrier of L
[(L "/\" C),(L "/\" p)] is set
the L_join of L . [(L "/\" C),(L "/\" p)] is set
C "\/" p is Element of the carrier of L
L "/\" (C "\/" p) is Element of the carrier of L
the L_meet of L . (L,(C "\/" p)) is Element of the carrier of L
[L,(C "\/" p)] is set
the L_meet of L . [L,(C "\/" p)] is set
L "/\" C is Element of the carrier of L
L "/\" p is Element of the carrier of L
(L "/\" C) "\/" (L "/\" p) is Element of the carrier of L
the L_join of L . ((L "/\" C),(L "/\" p)) is Element of the carrier of L
[(L "/\" C),(L "/\" p)] is set
the L_join of L . [(L "/\" C),(L "/\" p)] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
L is Element of the carrier of L
C is Element of the carrier of L
p is Element of the carrier of L
the L_meet of L . (C,p) is Element of the carrier of L
[C,p] is set
the L_meet of L . [C,p] is set
the L_meet of L . (L,( the L_meet of L . (C,p))) is Element of the carrier of L
[L,( the L_meet of L . (C,p))] is set
the L_meet of L . [L,( the L_meet of L . (C,p))] is set
C "/\" p is Element of the carrier of L
L "/\" (C "/\" p) is Element of the carrier of L
the L_meet of L . (L,(C "/\" p)) is Element of the carrier of L
[L,(C "/\" p)] is set
the L_meet of L . [L,(C "/\" p)] is set
L "/\" C is Element of the carrier of L
the L_meet of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_meet of L . [L,C] is set
(L "/\" C) "/\" p is Element of the carrier of L
the L_meet of L . ((L "/\" C),p) is Element of the carrier of L
[(L "/\" C),p] is set
the L_meet of L . [(L "/\" C),p] is set
L "/\" L is Element of the carrier of L
the L_meet of L . (L,L) is Element of the carrier of L
[L,L] is set
the L_meet of L . [L,L] is set
(L "/\" L) "/\" C is Element of the carrier of L
the L_meet of L . ((L "/\" L),C) is Element of the carrier of L
[(L "/\" L),C] is set
the L_meet of L . [(L "/\" L),C] is set
((L "/\" L) "/\" C) "/\" p is Element of the carrier of L
the L_meet of L . (((L "/\" L) "/\" C),p) is Element of the carrier of L
[((L "/\" L) "/\" C),p] is set
the L_meet of L . [((L "/\" L) "/\" C),p] is set
(L "/\" C) "/\" L is Element of the carrier of L
the L_meet of L . ((L "/\" C),L) is Element of the carrier of L
[(L "/\" C),L] is set
the L_meet of L . [(L "/\" C),L] is set
((L "/\" C) "/\" L) "/\" p is Element of the carrier of L
the L_meet of L . (((L "/\" C) "/\" L),p) is Element of the carrier of L
[((L "/\" C) "/\" L),p] is set
the L_meet of L . [((L "/\" C) "/\" L),p] is set
L "/\" p is Element of the carrier of L
the L_meet of L . (L,p) is Element of the carrier of L
[L,p] is set
the L_meet of L . [L,p] is set
(L "/\" C) "/\" (L "/\" p) is Element of the carrier of L
the L_meet of L . ((L "/\" C),(L "/\" p)) is Element of the carrier of L
[(L "/\" C),(L "/\" p)] is set
the L_meet of L . [(L "/\" C),(L "/\" p)] is set
the L_meet of L . (( the L_meet of L . (L,C)),( the L_meet of L . (L,p))) is Element of the carrier of L
[( the L_meet of L . (L,C)),( the L_meet of L . (L,p))] is set
the L_meet of L . [( the L_meet of L . (L,C)),( the L_meet of L . (L,p))] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
L is Element of the carrier of L
C is Element of the carrier of L
the L_meet of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_meet of L . [L,C] is set
the L_join of L . (L,( the L_meet of L . (L,C))) is Element of the carrier of L
[L,( the L_meet of L . (L,C))] is set
the L_join of L . [L,( the L_meet of L . (L,C))] is set
L "/\" C is Element of the carrier of L
L "\/" (L "/\" C) is Element of the carrier of L
the L_join of L . (L,(L "/\" C)) is Element of the carrier of L
[L,(L "/\" C)] is set
the L_join of L . [L,(L "/\" C)] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
L is Element of the carrier of L
C is Element of the carrier of L
the L_join of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_join of L . [L,C] is set
the L_meet of L . (L,( the L_join of L . (L,C))) is Element of the carrier of L
[L,( the L_join of L . (L,C))] is set
the L_meet of L . [L,( the L_join of L . (L,C))] is set
L "\/" C is Element of the carrier of L
L "/\" (L "\/" C) is Element of the carrier of L
the L_meet of L . (L,(L "\/" C)) is Element of the carrier of L
[L,(L "\/" C)] is set
the L_meet of L . [L,(L "\/" C)] is set
L is non empty set
Fin L is preBoolean set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
K20(L, the carrier of L) is Relation-like set
K19(K20(L, the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
C is Element of Fin L
p is Relation-like L -defined the carrier of L -valued Function-like non empty V14(L) V18(L, the carrier of L) Element of K19(K20(L, the carrier of L))
the L_join of L $$ (C,p) is Element of the carrier of L
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
the L_meet of L $$ (C,p) is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
L is non empty set
Fin L is preBoolean set
K20(L, the carrier of L) is Relation-like set
K19(K20(L, the carrier of L)) is set
C is Element of L
p is Element of Fin L
q is Relation-like L -defined the carrier of L -valued Function-like non empty V14(L) V18(L, the carrier of L) Element of K19(K20(L, the carrier of L))
q . C is Element of the carrier of L
(L,L,p,q) is Element of the carrier of L
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L $$ (p,q) is Element of the carrier of L
(q . C) "\/" (L,L,p,q) is Element of the carrier of L
the L_join of L . ((q . C),(L,L,p,q)) is Element of the carrier of L
[(q . C),(L,L,p,q)] is set
the L_join of L . [(q . C),(L,L,p,q)] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
L is Element of the carrier of L
C is non empty set
Fin C is preBoolean set
K20(C, the carrier of L) is Relation-like set
K19(K20(C, the carrier of L)) is set
p is Element of Fin C
q is Relation-like C -defined the carrier of L -valued Function-like non empty V14(C) V18(C, the carrier of L) Element of K19(K20(C, the carrier of L))
(C,L,p,q) is Element of the carrier of L
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L $$ (p,q) is Element of the carrier of L
B is Element of C
q . B is Element of the carrier of L
(q . B) "\/" (C,L,p,q) is Element of the carrier of L
the L_join of L . ((q . B),(C,L,p,q)) is Element of the carrier of L
[(q . B),(C,L,p,q)] is set
the L_join of L . [(q . B),(C,L,p,q)] is set
L "\/" (C,L,p,q) is Element of the carrier of L
the L_join of L . (L,(C,L,p,q)) is Element of the carrier of L
[L,(C,L,p,q)] is set
the L_join of L . [L,(C,L,p,q)] is set
L "\/" (q . B) is Element of the carrier of L
the L_join of L . (L,(q . B)) is Element of the carrier of L
[L,(q . B)] is set
the L_join of L . [L,(q . B)] is set
(L "\/" (q . B)) "\/" (C,L,p,q) is Element of the carrier of L
the L_join of L . ((L "\/" (q . B)),(C,L,p,q)) is Element of the carrier of L
[(L "\/" (q . B)),(C,L,p,q)] is set
the L_join of L . [(L "\/" (q . B)),(C,L,p,q)] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
C is non empty set
Fin C is preBoolean set
K20(C, the carrier of L) is Relation-like set
K19(K20(C, the carrier of L)) is set
p is Element of Fin C
q is Relation-like C -defined the carrier of L -valued Function-like non empty V14(C) V18(C, the carrier of L) Element of K19(K20(C, the carrier of L))
L is Element of the carrier of L
(C,L,p,q) is Element of the carrier of L
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L $$ (p,q) is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
L is Element of the carrier of L
C is non empty set
Fin C is preBoolean set
K20(C, the carrier of L) is Relation-like set
K19(K20(C, the carrier of L)) is set
p is Element of Fin C
q is Relation-like C -defined the carrier of L -valued Function-like non empty V14(C) V18(C, the carrier of L) Element of K19(K20(C, the carrier of L))
(C,L,p,q) is Element of the carrier of L
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L $$ (p,q) is Element of the carrier of L
B is Element of C
q . B is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
L is Element of the carrier of L
C is non empty set
Fin C is preBoolean set
K20(C, the carrier of L) is Relation-like set
K19(K20(C, the carrier of L)) is set
p is Element of Fin C
q is Relation-like C -defined the carrier of L -valued Function-like non empty V14(C) V18(C, the carrier of L) Element of K19(K20(C, the carrier of L))
(C,L,p,q) is Element of the carrier of L
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L $$ (p,q) is Element of the carrier of L
B is Element of C
q . B is Element of the carrier of L
the L_join of L [:] (q,L) is Relation-like C -defined the carrier of L -valued Function-like non empty V14(C) V18(C, the carrier of L) Element of K19(K20(C, the carrier of L))
( the L_join of L [:] (q,L)) . B is Element of the carrier of L
(q . B) "\/" L is Element of the carrier of L
the L_join of L . ((q . B),L) is Element of the carrier of L
[(q . B),L] is set
the L_join of L . [(q . B),L] is set
(C,L,p,q) "\/" L is Element of the carrier of L
the L_join of L . ((C,L,p,q),L) is Element of the carrier of L
[(C,L,p,q),L] is set
the L_join of L . [(C,L,p,q),L] is set
the L_join of L $$ (p,( the L_join of L [:] (q,L))) is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
L is non empty set
Fin L is preBoolean set
K20(L, the carrier of L) is Relation-like set
K19(K20(L, the carrier of L)) is set
C is Element of Fin L
p is Relation-like L -defined the carrier of L -valued Function-like non empty V14(L) V18(L, the carrier of L) Element of K19(K20(L, the carrier of L))
(L,L,C,p) is Element of the carrier of L
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L $$ (C,p) is Element of the carrier of L
q is Relation-like L -defined the carrier of L -valued Function-like non empty V14(L) V18(L, the carrier of L) Element of K19(K20(L, the carrier of L))
(L,L,C,q) is Element of the carrier of L
the L_join of L $$ (C,q) is Element of the carrier of L
B is Element of L
p . B is Element of the carrier of L
q . B is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
L is non empty set
Fin L is preBoolean set
K20(L, the carrier of L) is Relation-like set
K19(K20(L, the carrier of L)) is set
C is Element of Fin L
p is Relation-like L -defined the carrier of L -valued Function-like non empty V14(L) V18(L, the carrier of L) Element of K19(K20(L, the carrier of L))
p | C is Relation-like L -defined C -defined L -defined the carrier of L -valued Function-like Element of K19(K20(L, the carrier of L))
(L,L,C,p) is Element of the carrier of L
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L $$ (C,p) is Element of the carrier of L
q is Relation-like L -defined the carrier of L -valued Function-like non empty V14(L) V18(L, the carrier of L) Element of K19(K20(L, the carrier of L))
q | C is Relation-like L -defined C -defined L -defined the carrier of L -valued Function-like Element of K19(K20(L, the carrier of L))
(L,L,C,q) is Element of the carrier of L
the L_join of L $$ (C,q) is Element of the carrier of L
p .: C is Element of Fin the carrier of L
Fin the carrier of L is preBoolean set
q .: C is Element of Fin the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
C is non empty set
Fin C is preBoolean set
K20(C, the carrier of L) is Relation-like set
K19(K20(C, the carrier of L)) is set
p is Element of Fin C
L is Element of the carrier of L
q is Relation-like C -defined the carrier of L -valued Function-like non empty V14(C) V18(C, the carrier of L) Element of K19(K20(C, the carrier of L))
(C,L,p,q) is Element of the carrier of L
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L $$ (p,q) is Element of the carrier of L
L "\/" (C,L,p,q) is Element of the carrier of L
the L_join of L . (L,(C,L,p,q)) is Element of the carrier of L
[L,(C,L,p,q)] is set
the L_join of L . [L,(C,L,p,q)] is set
the L_join of L [;] (L,q) is Relation-like C -defined the carrier of L -valued Function-like non empty V14(C) V18(C, the carrier of L) Element of K19(K20(C, the carrier of L))
(C,L,p,( the L_join of L [;] (L,q))) is Element of the carrier of L
the L_join of L $$ (p,( the L_join of L [;] (L,q))) is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(L) is non empty strict LattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
the carrier of (L) is non empty set
the L_join of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
K20( the carrier of (L), the carrier of (L)) is Relation-like set
K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) is Relation-like set
K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L))) is set
the L_meet of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
L is non empty set
Fin L is preBoolean set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
K20(L, the carrier of L) is Relation-like set
K19(K20(L, the carrier of L)) is set
(L) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
the carrier of (L) is non empty set
K20(L, the carrier of (L)) is Relation-like set
K19(K20(L, the carrier of (L))) is set
p is Relation-like L -defined the carrier of L -valued Function-like non empty V14(L) V18(L, the carrier of L) Element of K19(K20(L, the carrier of L))
q is Relation-like L -defined the carrier of (L) -valued Function-like non empty V14(L) V18(L, the carrier of (L)) Element of K19(K20(L, the carrier of (L)))
C is Element of Fin L
(L,L,C,p) is Element of the carrier of L
the L_join of L $$ (C,p) is Element of the carrier of L
(L,(L),C,q) is Element of the carrier of (L)
the L_meet of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) commutative associative idempotent Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
K20( the carrier of (L), the carrier of (L)) is Relation-like set
K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) is Relation-like set
K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L))) is set
the L_meet of (L) $$ (C,q) is Element of the carrier of (L)
(L,L,C,p) is Element of the carrier of L
the L_meet of L $$ (C,p) is Element of the carrier of L
(L,(L),C,q) is Element of the carrier of (L)
the L_join of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) commutative associative idempotent Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
the L_join of (L) $$ (C,q) is Element of the carrier of (L)
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
(L) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
the carrier of (L) is non empty set
L is Element of the carrier of L
p is Element of the carrier of (L)
C is Element of the carrier of L
q is Element of the carrier of (L)
L "/\" C is Element of the carrier of L
the L_meet of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_meet of L . [L,C] is set
p "\/" q is Element of the carrier of (L)
the L_join of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) commutative associative idempotent Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
K20( the carrier of (L), the carrier of (L)) is Relation-like set
K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) is Relation-like set
K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L))) is set
the L_join of (L) . (p,q) is Element of the carrier of (L)
[p,q] is set
the L_join of (L) . [p,q] is set
L "\/" C is Element of the carrier of L
the L_join of L . (L,C) is Element of the carrier of L
the L_join of L . [L,C] is set
p "/\" q is Element of the carrier of (L)
the L_meet of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) commutative associative idempotent Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
the L_meet of (L) . (p,q) is Element of the carrier of (L)
the L_meet of (L) . [p,q] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
(L) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
the carrier of (L) is non empty set
L is Element of the carrier of L
C is Element of the carrier of L
L "\/" C is Element of the carrier of L
the L_join of L . (L,C) is Element of the carrier of L
[L,C] is set
the L_join of L . [L,C] is set
p is Element of the carrier of (L)
q is Element of the carrier of (L)
q "/\" p is Element of the carrier of (L)
the L_meet of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) commutative associative idempotent Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
K20( the carrier of (L), the carrier of (L)) is Relation-like set
K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) is Relation-like set
K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L))) is set
the L_meet of (L) . (q,p) is Element of the carrier of (L)
[q,p] is set
the L_meet of (L) . [q,p] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
(L) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
the carrier of (L) is non empty set
L is Element of the carrier of L
C is Element of the carrier of L
p is Element of the carrier of (L)
q is Element of the carrier of (L)
p "\/" q is Element of the carrier of (L)
the L_join of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) commutative associative idempotent Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
K20( the carrier of (L), the carrier of (L)) is Relation-like set
K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) is Relation-like set
K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L))) is set
the L_join of (L) . (p,q) is Element of the carrier of (L)
[p,q] is set
the L_join of (L) . [p,q] is set
C "/\" L is Element of the carrier of L
the L_meet of L . (C,L) is Element of the carrier of L
[C,L] is set
the L_meet of L . [C,L] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
L is non empty set
Fin L is preBoolean set
K20(L, the carrier of L) is Relation-like set
K19(K20(L, the carrier of L)) is set
C is Element of L
p is Element of Fin L
q is Relation-like L -defined the carrier of L -valued Function-like non empty V14(L) V18(L, the carrier of L) Element of K19(K20(L, the carrier of L))
(L,L,p,q) is Element of the carrier of L
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L $$ (p,q) is Element of the carrier of L
q . C is Element of the carrier of L
(L) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
the carrier of (L) is non empty set
K20(L, the carrier of (L)) is Relation-like set
K19(K20(L, the carrier of (L))) is set
B is Relation-like L -defined the carrier of (L) -valued Function-like non empty V14(L) V18(L, the carrier of (L)) Element of K19(K20(L, the carrier of (L)))
B . C is Element of the carrier of (L)
(L,(L),p,B) is Element of the carrier of (L)
the L_join of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) commutative associative idempotent Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
K20( the carrier of (L), the carrier of (L)) is Relation-like set
K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) is Relation-like set
K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L))) is set
the L_join of (L) $$ (p,B) is Element of the carrier of (L)
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
L is Element of the carrier of L
C is non empty set
Fin C is preBoolean set
K20(C, the carrier of L) is Relation-like set
K19(K20(C, the carrier of L)) is set
p is Element of Fin C
q is Relation-like C -defined the carrier of L -valued Function-like non empty V14(C) V18(C, the carrier of L) Element of K19(K20(C, the carrier of L))
(C,L,p,q) is Element of the carrier of L
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L $$ (p,q) is Element of the carrier of L
B is Element of C
q . B is Element of the carrier of L
(L) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
the carrier of (L) is non empty set
K20(C, the carrier of (L)) is Relation-like set
K19(K20(C, the carrier of (L))) is set
B is Element of the carrier of (L)
r is Relation-like C -defined the carrier of (L) -valued Function-like non empty V14(C) V18(C, the carrier of (L)) Element of K19(K20(C, the carrier of (L)))
r . B is Element of the carrier of (L)
(C,(L),p,r) is Element of the carrier of (L)
the L_join of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) commutative associative idempotent Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
K20( the carrier of (L), the carrier of (L)) is Relation-like set
K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) is Relation-like set
K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L))) is set
the L_join of (L) $$ (p,r) is Element of the carrier of (L)
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
C is non empty set
Fin C is preBoolean set
K20(C, the carrier of L) is Relation-like set
K19(K20(C, the carrier of L)) is set
p is Element of Fin C
q is Relation-like C -defined the carrier of L -valued Function-like non empty V14(C) V18(C, the carrier of L) Element of K19(K20(C, the carrier of L))
L is Element of the carrier of L
(C,L,p,q) is Element of the carrier of L
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L $$ (p,q) is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
C is non empty set
Fin C is preBoolean set
K20(C, the carrier of L) is Relation-like set
K19(K20(C, the carrier of L)) is set
p is Element of Fin C
L is Element of the carrier of L
q is Relation-like C -defined the carrier of L -valued Function-like non empty V14(C) V18(C, the carrier of L) Element of K19(K20(C, the carrier of L))
(C,L,p,q) is Element of the carrier of L
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L $$ (p,q) is Element of the carrier of L
L "/\" (C,L,p,q) is Element of the carrier of L
the L_meet of L . (L,(C,L,p,q)) is Element of the carrier of L
[L,(C,L,p,q)] is set
the L_meet of L . [L,(C,L,p,q)] is set
the L_meet of L [;] (L,q) is Relation-like C -defined the carrier of L -valued Function-like non empty V14(C) V18(C, the carrier of L) Element of K19(K20(C, the carrier of L))
(C,L,p,( the L_meet of L [;] (L,q))) is Element of the carrier of L
the L_meet of L $$ (p,( the L_meet of L [;] (L,q))) is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
L is Element of the carrier of L
C is non empty set
Fin C is preBoolean set
K20(C, the carrier of L) is Relation-like set
K19(K20(C, the carrier of L)) is set
p is Element of Fin C
q is Relation-like C -defined the carrier of L -valued Function-like non empty V14(C) V18(C, the carrier of L) Element of K19(K20(C, the carrier of L))
(C,L,p,q) is Element of the carrier of L
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L $$ (p,q) is Element of the carrier of L
B is Element of C
q . B is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
L is non empty set
Fin L is preBoolean set
K20(L, the carrier of L) is Relation-like set
K19(K20(L, the carrier of L)) is set
C is Element of Fin L
p is Relation-like L -defined the carrier of L -valued Function-like non empty V14(L) V18(L, the carrier of L) Element of K19(K20(L, the carrier of L))
p | C is Relation-like L -defined C -defined L -defined the carrier of L -valued Function-like Element of K19(K20(L, the carrier of L))
(L,L,C,p) is Element of the carrier of L
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L $$ (C,p) is Element of the carrier of L
q is Relation-like L -defined the carrier of L -valued Function-like non empty V14(L) V18(L, the carrier of L) Element of K19(K20(L, the carrier of L))
q | C is Relation-like L -defined C -defined L -defined the carrier of L -valued Function-like Element of K19(K20(L, the carrier of L))
(L,L,C,q) is Element of the carrier of L
the L_meet of L $$ (C,q) is Element of the carrier of L
(L) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
the carrier of (L) is non empty set
K20(L, the carrier of (L)) is Relation-like set
K19(K20(L, the carrier of (L))) is set
B is Relation-like L -defined the carrier of (L) -valued Function-like non empty V14(L) V18(L, the carrier of (L)) Element of K19(K20(L, the carrier of (L)))
(L,(L),C,B) is Element of the carrier of (L)
the L_join of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) commutative associative idempotent Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
K20( the carrier of (L), the carrier of (L)) is Relation-like set
K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) is Relation-like set
K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L))) is set
the L_join of (L) $$ (C,B) is Element of the carrier of (L)
B is Relation-like L -defined the carrier of (L) -valued Function-like non empty V14(L) V18(L, the carrier of (L)) Element of K19(K20(L, the carrier of (L)))
(L,(L),C,B) is Element of the carrier of (L)
the L_join of (L) $$ (C,B) is Element of the carrier of (L)
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
L is Element of the carrier of L
C is non empty set
Fin C is preBoolean set
K20(C, the carrier of L) is Relation-like set
K19(K20(C, the carrier of L)) is set
p is Element of Fin C
q is Relation-like C -defined the carrier of L -valued Function-like non empty V14(C) V18(C, the carrier of L) Element of K19(K20(C, the carrier of L))
(C,L,p,q) is Element of the carrier of L
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L $$ (p,q) is Element of the carrier of L
(L) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
the carrier of (L) is non empty set
K20(C, the carrier of (L)) is Relation-like set
K19(K20(C, the carrier of (L))) is set
B is Relation-like C -defined the carrier of (L) -valued Function-like non empty V14(C) V18(C, the carrier of (L)) Element of K19(K20(C, the carrier of (L)))
B is Element of the carrier of (L)
r is Element of C
B . r is Element of the carrier of (L)
(C,(L),p,B) is Element of the carrier of (L)
the L_join of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) commutative associative idempotent Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
K20( the carrier of (L), the carrier of (L)) is Relation-like set
K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) is Relation-like set
K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L))) is set
the L_join of (L) $$ (p,B) is Element of the carrier of (L)
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
L is non empty set
Fin L is preBoolean set
K20(L, the carrier of L) is Relation-like set
K19(K20(L, the carrier of L)) is set
C is Element of Fin L
p is Relation-like L -defined the carrier of L -valued Function-like non empty V14(L) V18(L, the carrier of L) Element of K19(K20(L, the carrier of L))
(L,L,C,p) is Element of the carrier of L
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L $$ (C,p) is Element of the carrier of L
q is Relation-like L -defined the carrier of L -valued Function-like non empty V14(L) V18(L, the carrier of L) Element of K19(K20(L, the carrier of L))
(L,L,C,q) is Element of the carrier of L
the L_meet of L $$ (C,q) is Element of the carrier of L
B is Element of L
p . B is Element of the carrier of L
q . B is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(L) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
L is Element of the carrier of L
the carrier of (L) is non empty set
C is Element of the carrier of (L)
p is Element of the carrier of (L)
C "\/" p is Element of the carrier of (L)
the L_join of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) commutative associative idempotent Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
K20( the carrier of (L), the carrier of (L)) is Relation-like set
K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) is Relation-like set
K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L))) is set
the L_join of (L) . (C,p) is Element of the carrier of (L)
[C,p] is set
the L_join of (L) . [C,p] is set
p "\/" C is Element of the carrier of (L)
the L_join of (L) . (p,C) is Element of the carrier of (L)
[p,C] is set
the L_join of (L) . [p,C] is set
C "\/" p is Element of the carrier of (L)
q is Element of the carrier of L
L "/\" q is Element of the carrier of L
the L_meet of L . (L,q) is Element of the carrier of L
[L,q] is set
the L_meet of L . [L,q] is set
p "\/" C is Element of the carrier of (L)
the carrier of (L) is non empty set
L is Element of the carrier of (L)
C is Element of the carrier of L
p is Element of the carrier of L
C "/\" p is Element of the carrier of L
the L_meet of L . (C,p) is Element of the carrier of L
[C,p] is set
the L_meet of L . [C,p] is set
p "/\" C is Element of the carrier of L
the L_meet of L . (p,C) is Element of the carrier of L
[p,C] is set
the L_meet of L . [p,C] is set
C "/\" p is Element of the carrier of L
q is Element of the carrier of (L)
L "\/" q is Element of the carrier of (L)
the L_join of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) commutative associative idempotent Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
K20( the carrier of (L), the carrier of (L)) is Relation-like set
K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) is Relation-like set
K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L))) is set
the L_join of (L) . (L,q) is Element of the carrier of (L)
[L,q] is set
the L_join of (L) . [L,q] is set
p "/\" C is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(L) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
L is Element of the carrier of L
the carrier of (L) is non empty set
C is Element of the carrier of (L)
p is Element of the carrier of (L)
C "/\" p is Element of the carrier of (L)
the L_meet of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) commutative associative idempotent Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
K20( the carrier of (L), the carrier of (L)) is Relation-like set
K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) is Relation-like set
K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L))) is set
the L_meet of (L) . (C,p) is Element of the carrier of (L)
[C,p] is set
the L_meet of (L) . [C,p] is set
p "/\" C is Element of the carrier of (L)
the L_meet of (L) . (p,C) is Element of the carrier of (L)
[p,C] is set
the L_meet of (L) . [p,C] is set
C "/\" p is Element of the carrier of (L)
q is Element of the carrier of L
L "\/" q is Element of the carrier of L
the L_join of L . (L,q) is Element of the carrier of L
[L,q] is set
the L_join of L . [L,q] is set
p "/\" C is Element of the carrier of (L)
the carrier of (L) is non empty set
L is Element of the carrier of (L)
C is Element of the carrier of L
p is Element of the carrier of L
C "\/" p is Element of the carrier of L
the L_join of L . (C,p) is Element of the carrier of L
[C,p] is set
the L_join of L . [C,p] is set
p "\/" C is Element of the carrier of L
the L_join of L . (p,C) is Element of the carrier of L
[p,C] is set
the L_join of L . [p,C] is set
C "\/" p is Element of the carrier of L
q is Element of the carrier of (L)
L "/\" q is Element of the carrier of (L)
the L_meet of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) commutative associative idempotent Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
K20( the carrier of (L), the carrier of (L)) is Relation-like set
K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) is Relation-like set
K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L))) is set
the L_meet of (L) . (L,q) is Element of the carrier of (L)
[L,q] is set
the L_meet of (L) . [L,q] is set
p "\/" C is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(L) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(L) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of L is non empty set
Bottom L is Element of the carrier of L
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
L is Element of the carrier of L
the L_join of L . ((Bottom L),L) is Element of the carrier of L
[(Bottom L),L] is set
the L_join of L . [(Bottom L),L] is set
(Bottom L) "\/" L is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of L is non empty set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
Bottom L is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
Bottom L is Element of the carrier of L
the carrier of L is non empty set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the_unity_wrt the L_join of L is Element of the carrier of L
L is non empty set
Fin L is preBoolean set
L is Element of Fin L
C is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of C is non empty set
K20(L, the carrier of C) is Relation-like set
K19(K20(L, the carrier of C)) is set
p is Relation-like L -defined the carrier of C -valued Function-like non empty V14(L) V18(L, the carrier of C) Element of K19(K20(L, the carrier of C))
p | L is Relation-like L -defined L -defined L -defined the carrier of C -valued Function-like Element of K19(K20(L, the carrier of C))
(L,C,L,p) is Element of the carrier of C
the L_join of C is Relation-like K20( the carrier of C, the carrier of C) -defined the carrier of C -valued Function-like V14(K20( the carrier of C, the carrier of C)) V18(K20( the carrier of C, the carrier of C), the carrier of C) commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of C, the carrier of C), the carrier of C))
K20( the carrier of C, the carrier of C) is Relation-like set
K20(K20( the carrier of C, the carrier of C), the carrier of C) is Relation-like set
K19(K20(K20( the carrier of C, the carrier of C), the carrier of C)) is set
the L_join of C $$ (L,p) is Element of the carrier of C
q is Relation-like L -defined the carrier of C -valued Function-like non empty V14(L) V18(L, the carrier of C) Element of K19(K20(L, the carrier of C))
q | L is Relation-like L -defined L -defined L -defined the carrier of C -valued Function-like Element of K19(K20(L, the carrier of C))
(L,C,L,q) is Element of the carrier of C
the L_join of C $$ (L,q) is Element of the carrier of C
Bottom C is Element of the carrier of C
the_unity_wrt the L_join of C is Element of the carrier of C
{}. L is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Element of Fin L
the L_join of C $$ (({}. L),p) is Element of the carrier of C
the L_join of C $$ (({}. L),q) is Element of the carrier of C
L is non empty set
Fin L is preBoolean set
L is Element of Fin L
C is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of C is non empty set
K20(L, the carrier of C) is Relation-like set
K19(K20(L, the carrier of C)) is set
p is Relation-like L -defined the carrier of C -valued Function-like non empty V14(L) V18(L, the carrier of C) Element of K19(K20(L, the carrier of C))
(L,C,L,p) is Element of the carrier of C
the L_join of C is Relation-like K20( the carrier of C, the carrier of C) -defined the carrier of C -valued Function-like V14(K20( the carrier of C, the carrier of C)) V18(K20( the carrier of C, the carrier of C), the carrier of C) commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of C, the carrier of C), the carrier of C))
K20( the carrier of C, the carrier of C) is Relation-like set
K20(K20( the carrier of C, the carrier of C), the carrier of C) is Relation-like set
K19(K20(K20( the carrier of C, the carrier of C), the carrier of C)) is set
the L_join of C $$ (L,p) is Element of the carrier of C
q is Element of the carrier of C
Bottom C is Element of the carrier of C
the_unity_wrt the L_join of C is Element of the carrier of C
{}. L is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Element of Fin L
the L_join of C $$ (({}. L),p) is Element of the carrier of C
L is non empty set
Fin L is preBoolean set
L is Element of Fin L
C is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of C is non empty set
K20(L, the carrier of C) is Relation-like set
K19(K20(L, the carrier of C)) is set
p is Relation-like L -defined the carrier of C -valued Function-like non empty V14(L) V18(L, the carrier of C) Element of K19(K20(L, the carrier of C))
(L,C,L,p) is Element of the carrier of C
the L_join of C is Relation-like K20( the carrier of C, the carrier of C) -defined the carrier of C -valued Function-like V14(K20( the carrier of C, the carrier of C)) V18(K20( the carrier of C, the carrier of C), the carrier of C) commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of C, the carrier of C), the carrier of C))
K20( the carrier of C, the carrier of C) is Relation-like set
K20(K20( the carrier of C, the carrier of C), the carrier of C) is Relation-like set
K19(K20(K20( the carrier of C, the carrier of C), the carrier of C)) is set
the L_join of C $$ (L,p) is Element of the carrier of C
q is Relation-like L -defined the carrier of C -valued Function-like non empty V14(L) V18(L, the carrier of C) Element of K19(K20(L, the carrier of C))
(L,C,L,q) is Element of the carrier of C
the L_join of C $$ (L,q) is Element of the carrier of C
B is Element of L
p . B is Element of the carrier of C
q . B is Element of the carrier of C
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of L is non empty set
Top L is Element of the carrier of L
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
L is Element of the carrier of L
the L_meet of L . ((Top L),L) is Element of the carrier of L
[(Top L),L] is set
the L_meet of L . [(Top L),L] is set
(Top L) "/\" L is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
Top L is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
Top L is Element of the carrier of L
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the_unity_wrt the L_meet of L is Element of the carrier of L
L is non empty set
Fin L is preBoolean set
L is Element of Fin L
C is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of C is non empty set
K20(L, the carrier of C) is Relation-like set
K19(K20(L, the carrier of C)) is set
p is Relation-like L -defined the carrier of C -valued Function-like non empty V14(L) V18(L, the carrier of C) Element of K19(K20(L, the carrier of C))
p | L is Relation-like L -defined L -defined L -defined the carrier of C -valued Function-like Element of K19(K20(L, the carrier of C))
(L,C,L,p) is Element of the carrier of C
the L_meet of C is Relation-like K20( the carrier of C, the carrier of C) -defined the carrier of C -valued Function-like V14(K20( the carrier of C, the carrier of C)) V18(K20( the carrier of C, the carrier of C), the carrier of C) commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of C, the carrier of C), the carrier of C))
K20( the carrier of C, the carrier of C) is Relation-like set
K20(K20( the carrier of C, the carrier of C), the carrier of C) is Relation-like set
K19(K20(K20( the carrier of C, the carrier of C), the carrier of C)) is set
the L_meet of C $$ (L,p) is Element of the carrier of C
q is Relation-like L -defined the carrier of C -valued Function-like non empty V14(L) V18(L, the carrier of C) Element of K19(K20(L, the carrier of C))
q | L is Relation-like L -defined L -defined L -defined the carrier of C -valued Function-like Element of K19(K20(L, the carrier of C))
(L,C,L,q) is Element of the carrier of C
the L_meet of C $$ (L,q) is Element of the carrier of C
(C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the L_join of C is Relation-like K20( the carrier of C, the carrier of C) -defined the carrier of C -valued Function-like V14(K20( the carrier of C, the carrier of C)) V18(K20( the carrier of C, the carrier of C), the carrier of C) commutative associative idempotent Element of K19(K20(K20( the carrier of C, the carrier of C), the carrier of C))
LattStr(# the carrier of C, the L_meet of C, the L_join of C #) is non empty strict LattStr
the carrier of (C) is non empty set
K20(L, the carrier of (C)) is Relation-like set
K19(K20(L, the carrier of (C))) is set
B is Relation-like L -defined the carrier of (C) -valued Function-like non empty V14(L) V18(L, the carrier of (C)) Element of K19(K20(L, the carrier of (C)))
(L,(C),L,B) is Element of the carrier of (C)
the L_join of (C) is Relation-like K20( the carrier of (C), the carrier of (C)) -defined the carrier of (C) -valued Function-like V14(K20( the carrier of (C), the carrier of (C))) V18(K20( the carrier of (C), the carrier of (C)), the carrier of (C)) commutative associative idempotent Element of K19(K20(K20( the carrier of (C), the carrier of (C)), the carrier of (C)))
K20( the carrier of (C), the carrier of (C)) is Relation-like set
K20(K20( the carrier of (C), the carrier of (C)), the carrier of (C)) is Relation-like set
K19(K20(K20( the carrier of (C), the carrier of (C)), the carrier of (C))) is set
the L_join of (C) $$ (L,B) is Element of the carrier of (C)
B is Relation-like L -defined the carrier of (C) -valued Function-like non empty V14(L) V18(L, the carrier of (C)) Element of K19(K20(L, the carrier of (C)))
(L,(C),L,B) is Element of the carrier of (C)
the L_join of (C) $$ (L,B) is Element of the carrier of (C)
L is non empty set
Fin L is preBoolean set
L is Element of Fin L
C is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of C is non empty set
K20(L, the carrier of C) is Relation-like set
K19(K20(L, the carrier of C)) is set
p is Relation-like L -defined the carrier of C -valued Function-like non empty V14(L) V18(L, the carrier of C) Element of K19(K20(L, the carrier of C))
(L,C,L,p) is Element of the carrier of C
the L_meet of C is Relation-like K20( the carrier of C, the carrier of C) -defined the carrier of C -valued Function-like V14(K20( the carrier of C, the carrier of C)) V18(K20( the carrier of C, the carrier of C), the carrier of C) commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of C, the carrier of C), the carrier of C))
K20( the carrier of C, the carrier of C) is Relation-like set
K20(K20( the carrier of C, the carrier of C), the carrier of C) is Relation-like set
K19(K20(K20( the carrier of C, the carrier of C), the carrier of C)) is set
the L_meet of C $$ (L,p) is Element of the carrier of C
q is Element of the carrier of C
(C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the L_join of C is Relation-like K20( the carrier of C, the carrier of C) -defined the carrier of C -valued Function-like V14(K20( the carrier of C, the carrier of C)) V18(K20( the carrier of C, the carrier of C), the carrier of C) commutative associative idempotent Element of K19(K20(K20( the carrier of C, the carrier of C), the carrier of C))
LattStr(# the carrier of C, the L_meet of C, the L_join of C #) is non empty strict LattStr
the carrier of (C) is non empty set
K20(L, the carrier of (C)) is Relation-like set
K19(K20(L, the carrier of (C))) is set
B is Relation-like L -defined the carrier of (C) -valued Function-like non empty V14(L) V18(L, the carrier of (C)) Element of K19(K20(L, the carrier of (C)))
B is Element of the carrier of (C)
r is Element of L
B . r is Element of the carrier of (C)
(L,(C),L,B) is Element of the carrier of (C)
the L_join of (C) is Relation-like K20( the carrier of (C), the carrier of (C)) -defined the carrier of (C) -valued Function-like V14(K20( the carrier of (C), the carrier of (C))) V18(K20( the carrier of (C), the carrier of (C)), the carrier of (C)) commutative associative idempotent Element of K19(K20(K20( the carrier of (C), the carrier of (C)), the carrier of (C)))
K20( the carrier of (C), the carrier of (C)) is Relation-like set
K20(K20( the carrier of (C), the carrier of (C)), the carrier of (C)) is Relation-like set
K19(K20(K20( the carrier of (C), the carrier of (C)), the carrier of (C))) is set
the L_join of (C) $$ (L,B) is Element of the carrier of (C)
L is non empty set
Fin L is preBoolean set
L is Element of Fin L
C is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of C is non empty set
K20(L, the carrier of C) is Relation-like set
K19(K20(L, the carrier of C)) is set
p is Relation-like L -defined the carrier of C -valued Function-like non empty V14(L) V18(L, the carrier of C) Element of K19(K20(L, the carrier of C))
(L,C,L,p) is Element of the carrier of C
the L_meet of C is Relation-like K20( the carrier of C, the carrier of C) -defined the carrier of C -valued Function-like V14(K20( the carrier of C, the carrier of C)) V18(K20( the carrier of C, the carrier of C), the carrier of C) commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of C, the carrier of C), the carrier of C))
K20( the carrier of C, the carrier of C) is Relation-like set
K20(K20( the carrier of C, the carrier of C), the carrier of C) is Relation-like set
K19(K20(K20( the carrier of C, the carrier of C), the carrier of C)) is set
the L_meet of C $$ (L,p) is Element of the carrier of C
q is Relation-like L -defined the carrier of C -valued Function-like non empty V14(L) V18(L, the carrier of C) Element of K19(K20(L, the carrier of C))
(L,C,L,q) is Element of the carrier of C
the L_meet of C $$ (L,q) is Element of the carrier of C
B is Element of L
p . B is Element of the carrier of C
q . B is Element of the carrier of C
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
Bottom L is Element of the carrier of L
the carrier of L is non empty set
(L) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
Top (L) is Element of the carrier of (L)
the carrier of (L) is non empty set
C is Element of the carrier of (L)
L is Element of the carrier of (L)
C "\/" L is Element of the carrier of (L)
the L_join of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) commutative associative idempotent Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
K20( the carrier of (L), the carrier of (L)) is Relation-like set
K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) is Relation-like set
K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L))) is set
the L_join of (L) . (C,L) is Element of the carrier of (L)
[C,L] is set
the L_join of (L) . [C,L] is set
p is Element of the carrier of L
(Bottom L) "/\" p is Element of the carrier of L
the L_meet of L . ((Bottom L),p) is Element of the carrier of L
[(Bottom L),p] is set
the L_meet of L . [(Bottom L),p] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
Top L is Element of the carrier of L
the carrier of L is non empty set
(L) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
Bottom (L) is Element of the carrier of (L)
the carrier of (L) is non empty set
C is Element of the carrier of (L)
L is Element of the carrier of (L)
C "/\" L is Element of the carrier of (L)
the L_meet of (L) is Relation-like K20( the carrier of (L), the carrier of (L)) -defined the carrier of (L) -valued Function-like V14(K20( the carrier of (L), the carrier of (L))) V18(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) commutative associative idempotent Element of K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)))
K20( the carrier of (L), the carrier of (L)) is Relation-like set
K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L)) is Relation-like set
K19(K20(K20( the carrier of (L), the carrier of (L)), the carrier of (L))) is set
the L_meet of (L) . (C,L) is Element of the carrier of (L)
[C,L] is set
the L_meet of (L) . [C,L] is set
p is Element of the carrier of L
(Top L) "\/" p is Element of the carrier of L
the L_join of L . ((Top L),p) is Element of the carrier of L
[(Top L),p] is set
the L_join of L . [(Top L),p] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
L is non empty set
Fin L is preBoolean set
L is Element of Fin L
C is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of C is non empty set
K20(L, the carrier of C) is Relation-like set
K19(K20(L, the carrier of C)) is set
the L_meet of C is Relation-like K20( the carrier of C, the carrier of C) -defined the carrier of C -valued Function-like V14(K20( the carrier of C, the carrier of C)) V18(K20( the carrier of C, the carrier of C), the carrier of C) commutative associative idempotent Element of K19(K20(K20( the carrier of C, the carrier of C), the carrier of C))
K20( the carrier of C, the carrier of C) is Relation-like set
K20(K20( the carrier of C, the carrier of C), the carrier of C) is Relation-like set
K19(K20(K20( the carrier of C, the carrier of C), the carrier of C)) is set
p is Relation-like L -defined the carrier of C -valued Function-like non empty V14(L) V18(L, the carrier of C) Element of K19(K20(L, the carrier of C))
(L,C,L,p) is Element of the carrier of C
the L_join of C is Relation-like K20( the carrier of C, the carrier of C) -defined the carrier of C -valued Function-like V14(K20( the carrier of C, the carrier of C)) V18(K20( the carrier of C, the carrier of C), the carrier of C) commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of C, the carrier of C), the carrier of C))
the L_join of C $$ (L,p) is Element of the carrier of C
q is Element of the carrier of C
the L_meet of C . (q,(L,C,L,p)) is Element of the carrier of C
[q,(L,C,L,p)] is set
the L_meet of C . [q,(L,C,L,p)] is set
the L_meet of C [;] (q,p) is Relation-like L -defined the carrier of C -valued Function-like non empty V14(L) V18(L, the carrier of C) Element of K19(K20(L, the carrier of C))
(L,C,L,( the L_meet of C [;] (q,p))) is Element of the carrier of C
the L_join of C $$ (L,( the L_meet of C [;] (q,p))) is Element of the carrier of C
Bottom C is Element of the carrier of C
the L_meet of C . (q,(Bottom C)) is Element of the carrier of C
[q,(Bottom C)] is set
the L_meet of C . [q,(Bottom C)] is set
q "/\" (Bottom C) is Element of the carrier of C
the_unity_wrt the L_join of C is Element of the carrier of C
L is non empty set
Fin L is preBoolean set
L is Element of Fin L
C is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of C is non empty set
K20(L, the carrier of C) is Relation-like set
K19(K20(L, the carrier of C)) is set
p is Relation-like L -defined the carrier of C -valued Function-like non empty V14(L) V18(L, the carrier of C) Element of K19(K20(L, the carrier of C))
(L,C,L,p) is Element of the carrier of C
the L_join of C is Relation-like K20( the carrier of C, the carrier of C) -defined the carrier of C -valued Function-like V14(K20( the carrier of C, the carrier of C)) V18(K20( the carrier of C, the carrier of C), the carrier of C) commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of C, the carrier of C), the carrier of C))
K20( the carrier of C, the carrier of C) is Relation-like set
K20(K20( the carrier of C, the carrier of C), the carrier of C) is Relation-like set
K19(K20(K20( the carrier of C, the carrier of C), the carrier of C)) is set
the L_join of C $$ (L,p) is Element of the carrier of C
q is Relation-like L -defined the carrier of C -valued Function-like non empty V14(L) V18(L, the carrier of C) Element of K19(K20(L, the carrier of C))
(L,C,L,q) is Element of the carrier of C
the L_join of C $$ (L,q) is Element of the carrier of C
B is Element of the carrier of C
B "/\" (L,C,L,q) is Element of the carrier of C
the L_meet of C is Relation-like K20( the carrier of C, the carrier of C) -defined the carrier of C -valued Function-like V14(K20( the carrier of C, the carrier of C)) V18(K20( the carrier of C, the carrier of C), the carrier of C) commutative associative idempotent Element of K19(K20(K20( the carrier of C, the carrier of C), the carrier of C))
the L_meet of C . (B,(L,C,L,q)) is Element of the carrier of C
[B,(L,C,L,q)] is set
the L_meet of C . [B,(L,C,L,q)] is set
the L_meet of C [;] (B,q) is Relation-like L -defined the carrier of C -valued Function-like non empty V14(L) V18(L, the carrier of C) Element of K19(K20(L, the carrier of C))
p | L is Relation-like L -defined L -defined L -defined the carrier of C -valued Function-like Element of K19(K20(L, the carrier of C))
( the L_meet of C [;] (B,q)) +* (p | L) is Relation-like L -defined the carrier of C -valued Function-like Element of K19(K20(L, the carrier of C))
dom (p | L) is set
B is Relation-like L -defined the carrier of C -valued Function-like non empty V14(L) V18(L, the carrier of C) Element of K19(K20(L, the carrier of C))
B | L is Relation-like L -defined L -defined L -defined the carrier of C -valued Function-like Element of K19(K20(L, the carrier of C))
r is Element of L
p . r is Element of the carrier of C
q . r is Element of the carrier of C
B "/\" (q . r) is Element of the carrier of C
the L_meet of C . (B,(q . r)) is Element of the carrier of C
[B,(q . r)] is set
the L_meet of C . [B,(q . r)] is set
( the L_meet of C [;] (B,q)) . r is Element of the carrier of C
(L,C,L,B) is Element of the carrier of C
the L_join of C $$ (L,B) is Element of the carrier of C
L is non empty set
Fin L is preBoolean set
C is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of C is non empty set
K20(L, the carrier of C) is Relation-like set
K19(K20(L, the carrier of C)) is set
q is Element of the carrier of C
L is Element of Fin L
p is Relation-like L -defined the carrier of C -valued Function-like non empty V14(L) V18(L, the carrier of C) Element of K19(K20(L, the carrier of C))
(L,C,L,p) is Element of the carrier of C
the L_join of C is Relation-like K20( the carrier of C, the carrier of C) -defined the carrier of C -valued Function-like V14(K20( the carrier of C, the carrier of C)) V18(K20( the carrier of C, the carrier of C), the carrier of C) commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of C, the carrier of C), the carrier of C))
K20( the carrier of C, the carrier of C) is Relation-like set
K20(K20( the carrier of C, the carrier of C), the carrier of C) is Relation-like set
K19(K20(K20( the carrier of C, the carrier of C), the carrier of C)) is set
the L_join of C $$ (L,p) is Element of the carrier of C
q "/\" (L,C,L,p) is Element of the carrier of C
the L_meet of C is Relation-like K20( the carrier of C, the carrier of C) -defined the carrier of C -valued Function-like V14(K20( the carrier of C, the carrier of C)) V18(K20( the carrier of C, the carrier of C), the carrier of C) commutative associative idempotent Element of K19(K20(K20( the carrier of C, the carrier of C), the carrier of C))
the L_meet of C . (q,(L,C,L,p)) is Element of the carrier of C
[q,(L,C,L,p)] is set
the L_meet of C . [q,(L,C,L,p)] is set
the L_meet of C [;] (q,p) is Relation-like L -defined the carrier of C -valued Function-like non empty V14(L) V18(L, the carrier of C) Element of K19(K20(L, the carrier of C))
(L,C,L,( the L_meet of C [;] (q,p))) is Element of the carrier of C
the L_join of C $$ (L,( the L_meet of C [;] (q,p))) is Element of the carrier of C
the non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative LattStr is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative LattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative () LattStr is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative () LattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of L is non empty set
L is Element of the carrier of L
C is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(L) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(L) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is non empty strict LattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
Fin the carrier of L is preBoolean set
L is Element of Fin the carrier of L
id the carrier of L is Relation-like the carrier of L -defined the carrier of L -valued Function-like one-to-one non empty V14( the carrier of L) V18( the carrier of L, the carrier of L) Element of K19(K20( the carrier of L, the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K19(K20( the carrier of L, the carrier of L)) is set
( the carrier of L,L,L,(id the carrier of L)) is Element of the carrier of L
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L $$ (L,(id the carrier of L)) is Element of the carrier of L
C is Element of the carrier of L
p is Element of the carrier of L
C "/\" p is Element of the carrier of L
the L_meet of L . (C,p) is Element of the carrier of L
[C,p] is set
the L_meet of L . [C,p] is set
p "/\" C is Element of the carrier of L
the L_meet of L . (p,C) is Element of the carrier of L
[p,C] is set
the L_meet of L . [p,C] is set
(id the carrier of L) . p is Element of the carrier of L
C "/\" p is Element of the carrier of L
p "/\" C is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
Fin the carrier of L is preBoolean set
L is Element of Fin the carrier of L
id the carrier of L is Relation-like the carrier of L -defined the carrier of L -valued Function-like one-to-one non empty V14( the carrier of L) V18( the carrier of L, the carrier of L) Element of K19(K20( the carrier of L, the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K19(K20( the carrier of L, the carrier of L)) is set
( the carrier of L,L,L,(id the carrier of L)) is Element of the carrier of L
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L $$ (L,(id the carrier of L)) is Element of the carrier of L
C is Element of the carrier of L
p is Element of the carrier of L
C "\/" p is Element of the carrier of L
the L_join of L . (C,p) is Element of the carrier of L
[C,p] is set
the L_join of L . [C,p] is set
p "\/" C is Element of the carrier of L
the L_join of L . (p,C) is Element of the carrier of L
[p,C] is set
the L_join of L . [p,C] is set
(id the carrier of L) . p is Element of the carrier of L
C "\/" p is Element of the carrier of L
p "\/" C is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of L is non empty set
p is Element of the carrier of L
q is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : S₁[b₁] } is set
Fin the carrier of L is preBoolean set
B is Element of Fin the carrier of L
id the carrier of L is Relation-like the carrier of L -defined the carrier of L -valued Function-like one-to-one non empty V14( the carrier of L) V18( the carrier of L, the carrier of L) Element of K19(K20( the carrier of L, the carrier of L))
K20( the carrier of L, the carrier of L) is Relation-like set
K19(K20( the carrier of L, the carrier of L)) is set
( the carrier of L,L,B,(id the carrier of L)) is Element of the carrier of L
the L_join of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
K20(K20( the carrier of L, the carrier of L), the carrier of L) is Relation-like set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L $$ (B,(id the carrier of L)) is Element of the carrier of L
r is Element of the carrier of L
p "/\" r is Element of the carrier of L
the L_meet of L is Relation-like K20( the carrier of L, the carrier of L) -defined the carrier of L -valued Function-like V14(K20( the carrier of L, the carrier of L)) V18(K20( the carrier of L, the carrier of L), the carrier of L) commutative associative idempotent Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))
the L_meet of L . (p,r) is Element of the carrier of L
[p,r] is set
the L_meet of L . [p,r] is set
r1 is Element of the carrier of L
the L_meet of L [;] (p,(id the carrier of L)) is Relation-like the carrier of L -defined the carrier of L -valued Function-like non empty V14( the carrier of L) V18( the carrier of L, the carrier of L) Element of K19(K20( the carrier of L, the carrier of L))
( the L_meet of L [;] (p,(id the carrier of L))) . r1 is Element of the carrier of L
(id the carrier of L) . r1 is Element of the carrier of L
the L_meet of L . (p,((id the carrier of L) . r1)) is Element of the carrier of L
[p,((id the carrier of L) . r1)] is set
the L_meet of L . [p,((id the carrier of L) . r1)] is set
p "/\" r1 is Element of the carrier of L
the L_meet of L . (p,r1) is Element of the carrier of L
[p,r1] is set
the L_meet of L . [p,r1] is set
c₁₀ is Element of the carrier of L
p "/\" c₁₀ is Element of the carrier of L
the L_meet of L . (p,c₁₀) is Element of the carrier of L
[p,c₁₀] is set
the L_meet of L . [p,c₁₀] is set
p "/\" r is Element of the carrier of L
( the carrier of L,L,B,( the L_meet of L [;] (p,(id the carrier of L)))) is Element of the carrier of L
the L_join of L $$ (B,( the L_meet of L [;] (p,(id the carrier of L)))) is Element of the carrier of L
r1 is Element of the carrier of L
p "/\" r1 is Element of the carrier of L
the L_meet of L . (p,r1) is Element of the carrier of L
[p,r1] is set
the L_meet of L . [p,r1] is set
p "/\" r1 is Element of the carrier of L
(id the carrier of L) . r1 is Element of the carrier of L