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