:: FILTER_2 semantic presentation

K121() is set

bool K121() is non empty set

K162() is set

bool K162() is non empty set

K166() is Element of bool K162()

[:K166(),K166():] is set

[:[:K166(),K166():],K166():] is set

bool [:[:K166(),K166():],K166():] is non empty set

Nat_Lattice is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr

the carrier of Nat_Lattice is non empty set

bool K166() is non empty set

NATPLUS is non empty Element of bool K166()

[:NATPLUS,NATPLUS:] is non empty set

[:[:NATPLUS,NATPLUS:],NATPLUS:] is non empty set

bool [:[:NATPLUS,NATPLUS:],NATPLUS:] is non empty set

{} is empty set

the empty set is empty set

1 is non empty set

L is non empty set

bool L is non empty set

[:L,L:] is non empty set

[:[:L,L:],L:] is non empty set

bool [:[:L,L:],L:] is non empty set

p is non empty Element of bool L

[:p,p:] is non empty set

[:[:p,p:],p:] is non empty set

bool [:[:p,p:],p:] is non empty set

q is Relation-like [:L,L:] -defined L -valued Function-like V18([:L,L:],L) Element of bool [:[:L,L:],L:]

q || p is Relation-like Function-like set

q | [:p,p:] is Relation-like set

K is Relation-like [:p,p:] -defined p -valued Function-like V18([:p,p:],p) Element of bool [:[:p,p:],p:]

dom K is Relation-like set

[:p,p:] is Relation-like L -defined L -valued non empty Element of bool [:L,L:]

bool [:L,L:] is non empty set

b9 is Element of p

b is Element of p

K . (b9,b) is Element of p

[b9,b] is set

{b9,b} is non empty set

{b9} is non empty set

{{b9,b},{b9}} is non empty set

K . [b9,b] is set

K . (b,b9) is Element of p

[b,b9] is set

{b,b9} is non empty set

{b} is non empty set

{{b,b9},{b}} is non empty set

K . [b,b9] is set

a is Element of p

a9 is Element of p

K . (b9,b) is Element of p

[b9,b] is Element of [:p,p:]

q . [b9,b] is set

c

c is Element of L

q . (c

[c

{c

{c

{{c

q . [c

q . (c,c

[c,c

{c,c

{c} is non empty set

{{c,c

q . [c,c

[b,b9] is Element of [:p,p:]

K . [b,b9] is set

K . (b,b9) is Element of p

b9 is Element of p

K . (b9,b9) is Element of p

[b9,b9] is set

{b9,b9} is non empty set

{b9} is non empty set

{{b9,b9},{b9}} is non empty set

K . [b9,b9] is set

K . (b9,b9) is Element of p

[b9,b9] is Element of [:p,p:]

q . [b9,b9] is set

q . (b9,b9) is Element of L

q . [b9,b9] is set

b9 is Element of p

b is Element of p

a is Element of p

K . (b,a) is Element of p

[b,a] is set

{b,a} is non empty set

{b} is non empty set

{{b,a},{b}} is non empty set

K . [b,a] is set

K . (b9,(K . (b,a))) is Element of p

[b9,(K . (b,a))] is set

{b9,(K . (b,a))} is non empty set

{b9} is non empty set

{{b9,(K . (b,a))},{b9}} is non empty set

K . [b9,(K . (b,a))] is set

K . (b9,b) is Element of p

[b9,b] is set

{b9,b} is non empty set

{{b9,b},{b9}} is non empty set

K . [b9,b] is set

K . ((K . (b9,b)),a) is Element of p

[(K . (b9,b)),a] is set

{(K . (b9,b)),a} is non empty set

{(K . (b9,b))} is non empty set

{{(K . (b9,b)),a},{(K . (b9,b))}} is non empty set

K . [(K . (b9,b)),a] is set

a9 is Element of p

c

c is Element of p

K . (b9,b) is Element of p

K . ((K . (b9,b)),a) is Element of p

[(K . (b9,b)),a] is set

{(K . (b9,b)),a} is non empty set

{(K . (b9,b))} is non empty set

{{(K . (b9,b)),a},{(K . (b9,b))}} is non empty set

K . [(K . (b9,b)),a] is set

[(K . (b9,b)),a] is Element of [:p,p:]

q . [(K . (b9,b)),a] is set

[b9,b] is Element of [:p,p:]

q . [b9,b] is set

[(q . [b9,b]),a] is set

{(q . [b9,b]),a} is non empty set

{(q . [b9,b])} is non empty set

{{(q . [b9,b]),a},{(q . [b9,b])}} is non empty set

q . [(q . [b9,b]),a] is set

q . (b9,b) is set

q . [b9,b] is set

q . ((q . (b9,b)),a) is set

[(q . (b9,b)),a] is set

{(q . (b9,b)),a} is non empty set

{(q . (b9,b))} is non empty set

{{(q . (b9,b)),a},{(q . (b9,b))}} is non empty set

q . [(q . (b9,b)),a] is set

d is Element of L

d9 is Element of L

e9 is Element of L

q . (d9,e9) is Element of L

[d9,e9] is set

{d9,e9} is non empty set

{d9} is non empty set

{{d9,e9},{d9}} is non empty set

q . [d9,e9] is set

q . (d,(q . (d9,e9))) is Element of L

[d,(q . (d9,e9))] is set

{d,(q . (d9,e9))} is non empty set

{d} is non empty set

{{d,(q . (d9,e9))},{d}} is non empty set

q . [d,(q . (d9,e9))] is set

[b,a] is Element of [:p,p:]

K . [b,a] is set

q . (b9,(K . [b,a])) is set

[b9,(K . [b,a])] is set

{b9,(K . [b,a])} is non empty set

{{b9,(K . [b,a])},{b9}} is non empty set

q . [b9,(K . [b,a])] is set

K . (b,a) is Element of p

[b9,(K . (b,a))] is Element of [:p,p:]

{b9,(K . (b,a))} is non empty set

{{b9,(K . (b,a))},{b9}} is non empty set

q . [b9,(K . (b,a))] is set

K . (b9,(K . (b,a))) is Element of p

[b9,(K . (b,a))] is set

K . [b9,(K . (b,a))] is set

L is non empty set

bool L is non empty set

[:L,L:] is non empty set

[:[:L,L:],L:] is non empty set

bool [:[:L,L:],L:] is non empty set

p is non empty Element of bool L

[:p,p:] is non empty set

[:[:p,p:],p:] is non empty set

bool [:[:p,p:],p:] is non empty set

q is Relation-like [:L,L:] -defined L -valued Function-like V18([:L,L:],L) Element of bool [:[:L,L:],L:]

q || p is Relation-like Function-like set

q | [:p,p:] is Relation-like set

K is Relation-like [:p,p:] -defined p -valued Function-like V18([:p,p:],p) Element of bool [:[:p,p:],p:]

b9 is Element of L

b is Element of p

dom K is Relation-like set

[:p,p:] is Relation-like L -defined L -valued non empty Element of bool [:L,L:]

bool [:L,L:] is non empty set

a is Element of p

K . (b,a) is Element of p

[b,a] is set

{b,a} is non empty set

{b} is non empty set

{{b,a},{b}} is non empty set

K . [b,a] is set

K . (b,a) is Element of p

[b,a] is Element of [:p,p:]

q . [b,a] is set

q . (b9,a) is Element of L

[b9,a] is set

{b9,a} is non empty set

{b9} is non empty set

{{b9,a},{b9}} is non empty set

q . [b9,a] is set

a is Element of p

K . (a,b) is Element of p

[a,b] is set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

K . [a,b] is set

K . (a,b) is Element of p

[a,b] is Element of [:p,p:]

q . [a,b] is set

q . (a,b9) is Element of L

[a,b9] is set

{a,b9} is non empty set

{{a,b9},{a}} is non empty set

q . [a,b9] is set

a is Element of p

[b,a] is Element of [:p,p:]

{b,a} is non empty set

{b} is non empty set

{{b,a},{b}} is non empty set

K . (b,a) is Element of p

[b,a] is set

K . [b,a] is set

a9 is Element of L

q . (b9,a9) is Element of L

[b9,a9] is set

{b9,a9} is non empty set

{b9} is non empty set

{{b9,a9},{b9}} is non empty set

q . [b9,a9] is set

[a,b] is Element of [:p,p:]

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

K . (a,b) is Element of p

[a,b] is set

K . [a,b] is set

q . (a9,b9) is Element of L

[a9,b9] is set

{a9,b9} is non empty set

{a9} is non empty set

{{a9,b9},{a9}} is non empty set

q . [a9,b9] is set

L is non empty set

bool L is non empty set

[:L,L:] is non empty set

[:[:L,L:],L:] is non empty set

bool [:[:L,L:],L:] is non empty set

p is non empty Element of bool L

[:p,p:] is non empty set

[:[:p,p:],p:] is non empty set

bool [:[:p,p:],p:] is non empty set

q is Relation-like [:L,L:] -defined L -valued Function-like V18([:L,L:],L) Element of bool [:[:L,L:],L:]

q || p is Relation-like Function-like set

q | [:p,p:] is Relation-like set

K is Relation-like [:L,L:] -defined L -valued Function-like V18([:L,L:],L) Element of bool [:[:L,L:],L:]

K || p is Relation-like Function-like set

K | [:p,p:] is Relation-like set

b9 is Relation-like [:p,p:] -defined p -valued Function-like V18([:p,p:],p) Element of bool [:[:p,p:],p:]

b is Relation-like [:p,p:] -defined p -valued Function-like V18([:p,p:],p) Element of bool [:[:p,p:],p:]

a is Element of p

a9 is Element of p

c

b . (a9,c

[a9,c

{a9,c

{a9} is non empty set

{{a9,c

b . [a9,c

b9 . (a,(b . (a9,c

[a,(b . (a9,c

{a,(b . (a9,c

{a} is non empty set

{{a,(b . (a9,c

b9 . [a,(b . (a9,c

b9 . (a,a9) is Element of p

[a,a9] is set

{a,a9} is non empty set

{{a,a9},{a}} is non empty set

b9 . [a,a9] is set

b9 . (a,c

[a,c

{a,c

{{a,c

b9 . [a,c

b . ((b9 . (a,a9)),(b9 . (a,c

[(b9 . (a,a9)),(b9 . (a,c

{(b9 . (a,a9)),(b9 . (a,c

{(b9 . (a,a9))} is non empty set

{{(b9 . (a,a9)),(b9 . (a,c

b . [(b9 . (a,a9)),(b9 . (a,c

b9 . (a,a9) is Element of p

b9 . (a,c

b . (a9,c

e is Element of L

ae is Element of L

[e,ae] is Element of [:L,L:]

{e,ae} is non empty set

{e} is non empty set

{{e,ae},{e}} is non empty set

K . [e,ae] is set

K . (e,ae) is Element of L

[e,ae] is set

K . [e,ae] is set

e9 is Element of L

[e9,e] is Element of [:L,L:]

{e9,e} is non empty set

{e9} is non empty set

{{e9,e},{e9}} is non empty set

q . [e9,e] is set

q . (e9,e) is Element of L

[e9,e] is set

q . [e9,e] is set

[e9,ae] is Element of [:L,L:]

{e9,ae} is non empty set

{{e9,ae},{e9}} is non empty set

q . [e9,ae] is set

q . (e9,ae) is Element of L

[e9,ae] is set

q . [e9,ae] is set

[a,(b . (a9,c

{a,(b . (a9,c

{{a,(b . (a9,c

q . [a,(b . (a9,c

q . (a,(b . (a9,c

[a,(b . (a9,c

q . [a,(b . (a9,c

dom b is Relation-like set

[:p,p:] is Relation-like L -defined L -valued non empty Element of bool [:L,L:]

bool [:L,L:] is non empty set

[a9,c

b . [a9,c

K . [a9,c

[(b9 . (a,a9)),(b9 . (a,c

{(b9 . (a,a9)),(b9 . (a,c

{(b9 . (a,a9))} is non empty set

{{(b9 . (a,a9)),(b9 . (a,c

b . [(b9 . (a,a9)),(b9 . (a,c

K . [(b9 . (a,a9)),(b9 . (a,c

K . ((b9 . (a,a9)),(b9 . (a,c

[(b9 . (a,a9)),(b9 . (a,c

K . [(b9 . (a,a9)),(b9 . (a,c

dom b9 is Relation-like set

b9 . [a,(b . (a9,c

[a,a9] is Element of [:p,p:]

b9 . [a,a9] is set

q . [a,a9] is set

[a,c

b9 . [a,c

q . [a,c

b9 . (a,(b . (a9,c

b9 . [a,(b . (a9,c

b . ((b9 . (a,a9)),(b9 . (a,c

b . [(b9 . (a,a9)),(b9 . (a,c

a is Element of p

a9 is Element of p

b . (a,a9) is Element of p

[a,a9] is set

{a,a9} is non empty set

{a} is non empty set

{{a,a9},{a}} is non empty set

b . [a,a9] is set

c

b9 . ((b . (a,a9)),c

[(b . (a,a9)),c

{(b . (a,a9)),c

{(b . (a,a9))} is non empty set

{{(b . (a,a9)),c

b9 . [(b . (a,a9)),c

b9 . (a,c

[a,c

{a,c

{{a,c

b9 . [a,c

b9 . (a9,c

[a9,c

{a9,c

{a9} is non empty set

{{a9,c

b9 . [a9,c

b . ((b9 . (a,c

[(b9 . (a,c

{(b9 . (a,c

{(b9 . (a,c

{{(b9 . (a,c

b . [(b9 . (a,c

b . (a,a9) is Element of p

b9 . (a,c

b9 . (a9,c

[(b9 . (a,c

{(b9 . (a,c

{(b9 . (a,c

{{(b9 . (a,c

K . [(b9 . (a,c

K . ((b9 . (a,c

[(b9 . (a,c

K . [(b9 . (a,c

dom b9 is Relation-like set

[:p,p:] is Relation-like L -defined L -valued non empty Element of bool [:L,L:]

bool [:L,L:] is non empty set

[(b . (a,a9)),c

{(b . (a,a9)),c

{(b . (a,a9))} is non empty set

{{(b . (a,a9)),c

b9 . [(b . (a,a9)),c

q . [(b . (a,a9)),c

dom b is Relation-like set

[a,a9] is Element of [:p,p:]

b . [a,a9] is set

K . [a,a9] is set

b . [(b9 . (a,c

e is Element of L

ae is Element of L

[e,ae] is Element of [:L,L:]

{e,ae} is non empty set

{e} is non empty set

{{e,ae},{e}} is non empty set

q . [e,ae] is set

q . (e,ae) is Element of L

[e,ae] is set

q . [e,ae] is set

e9 is Element of L

[e9,e] is Element of [:L,L:]

{e9,e} is non empty set

{e9} is non empty set

{{e9,e},{e9}} is non empty set

K . [e9,e] is set

K . (e9,e) is Element of L

[e9,e] is set

K . [e9,e] is set

[e9,ae] is Element of [:L,L:]

{e9,ae} is non empty set

{{e9,ae},{e9}} is non empty set

q . [e9,ae] is set

q . (e9,ae) is Element of L

[e9,ae] is set

q . [e9,ae] is set

q . ((b . (a,a9)),c

[(b . (a,a9)),c

q . [(b . (a,a9)),c

[a9,c

b9 . [a9,c

q . [a9,c

[a,c

b9 . [a,c

q . [a,c

b9 . ((b . (a,a9)),c

b9 . [(b . (a,a9)),c

b . ((b9 . (a,c

b . [(b9 . (a,c

L is non empty set

bool L is non empty set

[:L,L:] is non empty set

[:[:L,L:],L:] is non empty set

bool [:[:L,L:],L:] is non empty set

p is non empty Element of bool L

[:p,p:] is non empty set

[:[:p,p:],p:] is non empty set

bool [:[:p,p:],p:] is non empty set

q is Relation-like [:L,L:] -defined L -valued Function-like V18([:L,L:],L) Element of bool [:[:L,L:],L:]

q || p is Relation-like Function-like set

q | [:p,p:] is Relation-like set

K is Relation-like [:L,L:] -defined L -valued Function-like V18([:L,L:],L) Element of bool [:[:L,L:],L:]

K || p is Relation-like Function-like set

K | [:p,p:] is Relation-like set

b9 is Relation-like [:p,p:] -defined p -valued Function-like V18([:p,p:],p) Element of bool [:[:p,p:],p:]

b is Relation-like [:p,p:] -defined p -valued Function-like V18([:p,p:],p) Element of bool [:[:p,p:],p:]

L is non empty set

bool L is non empty set

[:L,L:] is non empty set

[:[:L,L:],L:] is non empty set

bool [:[:L,L:],L:] is non empty set

p is non empty Element of bool L

[:p,p:] is non empty set

[:[:p,p:],p:] is non empty set

bool [:[:p,p:],p:] is non empty set

q is Relation-like [:L,L:] -defined L -valued Function-like V18([:L,L:],L) Element of bool [:[:L,L:],L:]

q || p is Relation-like Function-like set

q | [:p,p:] is Relation-like set

K is Relation-like [:L,L:] -defined L -valued Function-like V18([:L,L:],L) Element of bool [:[:L,L:],L:]

K || p is Relation-like Function-like set

K | [:p,p:] is Relation-like set

b9 is Relation-like [:p,p:] -defined p -valued Function-like V18([:p,p:],p) Element of bool [:[:p,p:],p:]

b is Relation-like [:p,p:] -defined p -valued Function-like V18([:p,p:],p) Element of bool [:[:p,p:],p:]

a is Element of p

a9 is Element of p

b . (a,a9) is Element of p

[a,a9] is set

{a,a9} is non empty set

{a} is non empty set

{{a,a9},{a}} is non empty set

b . [a,a9] is set

b9 . (a,(b . (a,a9))) is Element of p

[a,(b . (a,a9))] is set

{a,(b . (a,a9))} is non empty set

{{a,(b . (a,a9))},{a}} is non empty set

b9 . [a,(b . (a,a9))] is set

dom b is Relation-like set

[:p,p:] is Relation-like L -defined L -valued non empty Element of bool [:L,L:]

bool [:L,L:] is non empty set

dom b9 is Relation-like set

[a,(b . (a,a9))] is Element of [:p,p:]

q . [a,(b . (a,a9))] is set

[a,a9] is Element of [:p,p:]

K . [a,a9] is set

[a,(K . [a,a9])] is set

{a,(K . [a,a9])} is non empty set

{{a,(K . [a,a9])},{a}} is non empty set

q . [a,(K . [a,a9])] is set

K . (a,a9) is Element of L

K . [a,a9] is set

q . (a,(K . (a,a9))) is Element of L

[a,(K . (a,a9))] is set

{a,(K . (a,a9))} is non empty set

{{a,(K . (a,a9))},{a}} is non empty set

q . [a,(K . (a,a9))] is set

L is non empty set

bool L is non empty set

p is Element of bool L

q is Element of bool L

K is Element of L

b9 is Element of L

L is LattStr

the carrier of L is set

the L_join of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the L_meet of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is strict LattStr

p is LattStr

the carrier of p is set

the L_join of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like V18([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

[: the carrier of p, the carrier of p:] is set

[:[: the carrier of p, the carrier of p:], the carrier of p:] is set

bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

the L_meet of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like V18([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

LattStr(# the carrier of p, the L_join of p, the L_meet of p #) is strict LattStr

L .: is strict LattStr

LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is strict LattStr

p .: is strict LattStr

LattStr(# the carrier of p, the L_meet of p, the L_join of p #) is 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 [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the L_join of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: 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 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 [: the carrier of (L .:), the carrier of (L .:):] -defined the carrier of (L .:) -valued Function-like V18([: the carrier of (L .:), the carrier of (L .:):], the carrier of (L .:)) commutative associative idempotent Element of bool [:[: the carrier of (L .:), the carrier of (L .:):], the carrier of (L .:):]

[: the carrier of (L .:), the carrier of (L .:):] is non empty set

[:[: the carrier of (L .:), the carrier of (L .:):], the carrier of (L .:):] is non empty set

bool [:[: the carrier of (L .:), the carrier of (L .:):], the carrier of (L .:):] is non empty set

the L_join of (L .:) is Relation-like [: the carrier of (L .:), the carrier of (L .:):] -defined the carrier of (L .:) -valued Function-like V18([: the carrier of (L .:), the carrier of (L .:):], the carrier of (L .:)) commutative associative idempotent Element of bool [:[: 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

LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr

L is non empty LattStr

the carrier of L is non empty set

the L_join of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the L_meet of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr

p is non empty LattStr

the carrier of p is non empty set

the L_join of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like V18([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

[: the carrier of p, the carrier of p:] is non empty set

[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

the L_meet of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like V18([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

LattStr(# the carrier of p, the L_join of p, the L_meet of p #) is non empty strict LattStr

q is Element of the carrier of L

K is Element of the carrier of L

q "\/" K is Element of the carrier of L

the L_join of L . (q,K) is Element of the carrier of L

[q,K] is set

{q,K} is non empty set

{q} is non empty set

{{q,K},{q}} is non empty set

the L_join of L . [q,K] is set

q "/\" K is Element of the carrier of L

the L_meet of L . (q,K) is Element of the carrier of L

the L_meet of L . [q,K] is set

b9 is Element of the carrier of p

b is Element of the carrier of p

b9 "\/" b is Element of the carrier of p

the L_join of p . (b9,b) is Element of the carrier of p

[b9,b] is set

{b9,b} is non empty set

{b9} is non empty set

{{b9,b},{b9}} is non empty set

the L_join of p . [b9,b] is set

b9 "/\" b is Element of the carrier of p

the L_meet of p . (b9,b) is Element of the carrier of p

the L_meet of p . [b9,b] is set

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 [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the L_meet of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr

p is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr

the carrier of p is non empty set

the L_join of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like V18([: the carrier of p, the carrier of p:], the carrier of p) commutative associative idempotent Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

[: the carrier of p, the carrier of p:] is non empty set

[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

the L_meet of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like V18([: the carrier of p, the carrier of p:], the carrier of p) commutative associative idempotent Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

LattStr(# the carrier of p, the L_join of p, the L_meet of p #) is non empty strict LattStr

Bottom L is Element of the carrier of L

Bottom p is Element of the carrier of p

K is Element of the carrier of p

b9 is Element of the carrier of L

(Bottom L) "/\" b9 is Element of the carrier of L

the L_meet of L . ((Bottom L),b9) is Element of the carrier of L

[(Bottom L),b9] is set

{(Bottom L),b9} is non empty set

{(Bottom L)} is non empty set

{{(Bottom L),b9},{(Bottom L)}} is non empty set

the L_meet of L . [(Bottom L),b9] is set

q is Element of the carrier of p

q "/\" K is Element of the carrier of p

the L_meet of p . (q,K) is Element of the carrier of p

[q,K] is set

{q,K} is non empty set

{q} is non empty set

{{q,K},{q}} is non empty set

the L_meet of p . [q,K] is set

K "/\" q is Element of the carrier of p

the L_meet of p . (K,q) is Element of the carrier of p

[K,q] is set

{K,q} is non empty set

{K} is non empty set

{{K,q},{K}} is non empty set

the L_meet of p . [K,q] is set

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_join of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the L_meet of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr

p is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr

the carrier of p is non empty set

the L_join of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like V18([: the carrier of p, the carrier of p:], the carrier of p) commutative associative idempotent Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

[: the carrier of p, the carrier of p:] is non empty set

[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

the L_meet of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like V18([: the carrier of p, the carrier of p:], the carrier of p) commutative associative idempotent Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

LattStr(# the carrier of p, the L_join of p, the L_meet of p #) is non empty strict LattStr

Top L is Element of the carrier of L

Top p is Element of the carrier of p

K is Element of the carrier of p

b9 is Element of the carrier of L

(Top L) "\/" b9 is Element of the carrier of L

the L_join of L . ((Top L),b9) is Element of the carrier of L

[(Top L),b9] is set

{(Top L),b9} is non empty set

{(Top L)} is non empty set

{{(Top L),b9},{(Top L)}} is non empty set

the L_join of L . [(Top L),b9] is set

q is Element of the carrier of p

q "\/" K is Element of the carrier of p

the L_join of p . (q,K) is Element of the carrier of p

[q,K] is set

{q,K} is non empty set

{q} is non empty set

{{q,K},{q}} is non empty set

the L_join of p . [q,K] is set

K "\/" q is Element of the carrier of p

the L_join of p . (K,q) is Element of the carrier of p

[K,q] is set

{K,q} is non empty set

{K} is non empty set

{{K,q},{K}} is non empty set

the L_join of p . [K,q] is set

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complemented LattStr

the carrier of L is non empty set

the L_join of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the L_meet of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr

p is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complemented LattStr

the carrier of p is non empty set

the L_join of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like V18([: the carrier of p, the carrier of p:], the carrier of p) commutative associative idempotent Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

[: the carrier of p, the carrier of p:] is non empty set

[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

the L_meet of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like V18([: the carrier of p, the carrier of p:], the carrier of p) commutative associative idempotent Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

LattStr(# the carrier of p, the L_join of p, the L_meet of p #) is non empty strict LattStr

q is Element of the carrier of L

K is Element of the carrier of L

b9 is Element of the carrier of p

b is Element of the carrier of p

b9 "\/" b is Element of the carrier of p

the L_join of p . (b9,b) is Element of the carrier of p

[b9,b] is set

{b9,b} is non empty set

{b9} is non empty set

{{b9,b},{b9}} is non empty set

the L_join of p . [b9,b] is set

q "\/" K is Element of the carrier of L

the L_join of L . (q,K) is Element of the carrier of L

[q,K] is set

{q,K} is non empty set

{q} is non empty set

{{q,K},{q}} is non empty set

the L_join of L . [q,K] is set

b9 "/\" b is Element of the carrier of p

the L_meet of p . (b9,b) is Element of the carrier of p

the L_meet of p . [b9,b] is set

q "/\" K is Element of the carrier of L

the L_meet of L . (q,K) is Element of the carrier of L

the L_meet of L . [q,K] is set

Top L is Element of the carrier of L

Bottom L is Element of the carrier of L

Top p is Element of the carrier of p

b "\/" b9 is Element of the carrier of p

the L_join of p . (b,b9) is Element of the carrier of p

[b,b9] is set

{b,b9} is non empty set

{b} is non empty set

{{b,b9},{b}} is non empty set

the L_join of p . [b,b9] is set

Bottom p is Element of the carrier of p

b "/\" b9 is Element of the carrier of p

the L_meet of p . (b,b9) is Element of the carrier of p

the L_meet of p . [b,b9] is set

L 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 Heyting LattStr

the carrier of L is non empty set

the L_join of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the L_meet of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr

p 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 Heyting LattStr

the carrier of p is non empty set

the L_join of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like V18([: the carrier of p, the carrier of p:], the carrier of p) commutative associative idempotent Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

[: the carrier of p, the carrier of p:] is non empty set

[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

the L_meet of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like V18([: the carrier of p, the carrier of p:], the carrier of p) commutative associative idempotent Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

LattStr(# the carrier of p, the L_join of p, the L_meet of p #) is non empty strict LattStr

q is Element of the carrier of L

q ` is Element of the carrier of L

K is Element of the carrier of p

K ` is Element of the carrier of p

b9 is Element of the carrier of p

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

bool the carrier of L is non empty set

p is Element of bool the carrier of L

q is Element of the carrier of L

K is Element of the carrier of L

q "\/" K is Element of the carrier of L

the L_join of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the L_join of L . (q,K) is Element of the carrier of L

[q,K] is set

{q,K} is non empty set

{q} is non empty set

{{q,K},{q}} is non empty set

the L_join of L . [q,K] is set

q "/\" (q "\/" K) is Element of the carrier of L

the L_meet of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

the L_meet of L . (q,(q "\/" K)) is Element of the carrier of L

[q,(q "\/" K)] is set

{q,(q "\/" K)} is non empty set

{{q,(q "\/" K)},{q}} is non empty set

the L_meet of L . [q,(q "\/" K)] 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

bool the carrier of L is non empty set

p is Element of bool the carrier of L

q is Element of the carrier of L

K is Element of the carrier of L

q "/\" K is Element of the carrier of L

the L_meet of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the L_meet of L . (q,K) is Element of the carrier of L

[q,K] is set

{q,K} is non empty set

{q} is non empty set

{{q,K},{q}} is non empty set

the L_meet of L . [q,K] is set

(q "/\" K) "\/" K is Element of the carrier of L

the L_join of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

the L_join of L . ((q "/\" K),K) is Element of the carrier of L

[(q "/\" K),K] is set

{(q "/\" K),K} is non empty set

{(q "/\" K)} is non empty set

{{(q "/\" K),K},{(q "/\" K)}} is non empty set

the L_join of L . [(q "/\" K),K] 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

bool the carrier of L is non empty set

p is non empty Element of bool the carrier of L

q is Element of the carrier of L

K is Element of the carrier of L

q "\/" K is Element of the carrier of L

the L_join of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the L_join of L . (q,K) is Element of the carrier of L

[q,K] is set

{q,K} is non empty set

{q} is non empty set

{{q,K},{q}} is non empty set

the L_join of L . [q,K] is set

q is Element of the carrier of L

K is Element of the carrier of L

q "\/" K is Element of the carrier of L

the L_join of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the L_join of L . (q,K) is Element of the carrier of L

[q,K] is set

{q,K} is non empty set

{q} is non empty set

{{q,K},{q}} is non empty set

the L_join of L . [q,K] 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 [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the L_meet of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr

p is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of p is non empty set

the L_join of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like V18([: the carrier of p, the carrier of p:], the carrier of p) commutative associative idempotent Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

[: the carrier of p, the carrier of p:] is non empty set

[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

the L_meet of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like V18([: the carrier of p, the carrier of p:], the carrier of p) commutative associative idempotent Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

LattStr(# the carrier of p, the L_join of p, the L_meet of p #) is non empty strict LattStr

bool the carrier of L is non empty set

bool the carrier of p is non empty set

q is set

b9 is Element of the carrier of p

b is Element of the carrier of p

b9 "/\" b is Element of the carrier of p

the L_meet of p . (b9,b) is Element of the carrier of p

[b9,b] is set

{b9,b} is non empty set

{b9} is non empty set

{{b9,b},{b9}} is non empty set

the L_meet of p . [b9,b] is set

a is Element of the carrier of L

a9 is Element of the carrier of L

a "/\" a9 is Element of the carrier of L

the L_meet of L . (a,a9) is Element of the carrier of L

[a,a9] is set

{a,a9} is non empty set

{a} is non empty set

{{a,a9},{a}} is non empty set

the L_meet of L . [a,a9] is set

K is non empty final meet-closed join-closed Element of bool 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 [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the L_meet of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is non empty strict LattStr

p is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of p is non empty set

the L_join of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like V18([: the carrier of p, the carrier of p:], the carrier of p) commutative associative idempotent Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

[: the carrier of p, the carrier of p:] is non empty set

[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

the L_meet of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like V18([: the carrier of p, the carrier of p:], the carrier of p) commutative associative idempotent Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

LattStr(# the carrier of p, the L_join of p, the L_meet of p #) is non empty strict LattStr

bool the carrier of L is non empty set

bool the carrier of p is non empty set

q is set

b9 is Element of the carrier of p

b is Element of the carrier of p

b9 "\/" b is Element of the carrier of p

the L_join of p . (b9,b) is Element of the carrier of p

[b9,b] is set

{b9,b} is non empty set

{b9} is non empty set

{{b9,b},{b9}} is non empty set

the L_join of p . [b9,b] is set

a is Element of the carrier of L

a9 is Element of the carrier of L

a "\/" a9 is Element of the carrier of L

the L_join of L . (a,a9) is Element of the carrier of L

[a,a9] is set

{a,a9} is non empty set

{a} is non empty set

{{a,a9},{a}} is non empty set

the L_join of L . [a,a9] is set

K is non empty initial meet-closed join-closed Element of bool 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

p 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_meet of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the L_join of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: 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 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 [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the L_join of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: 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

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

q is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

q .: is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of q is non empty set

the L_meet of q is Relation-like [: the carrier of q, the carrier of q:] -defined the carrier of q -valued Function-like V18([: the carrier of q, the carrier of q:], the carrier of q) commutative associative idempotent Element of bool [:[: the carrier of q, the carrier of q:], the carrier of q:]

[: the carrier of q, the carrier of q:] is non empty set

[:[: the carrier of q, the carrier of q:], the carrier of q:] is non empty set

bool [:[: the carrier of q, the carrier of q:], the carrier of q:] is non empty set

the L_join of q is Relation-like [: the carrier of q, the carrier of q:] -defined the carrier of q -valued Function-like V18([: the carrier of q, the carrier of q:], the carrier of q) commutative associative idempotent Element of bool [:[: the carrier of q, the carrier of q:], the carrier of q:]

LattStr(# the carrier of q, the L_meet of q, the L_join of q #) is non empty strict LattStr

the carrier of (q .:) is non empty set

p is Element of the carrier of L

(L,p) 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_meet of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the L_join of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: 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,(L,p)) is Element of the carrier of L

K is Element of the carrier of (q .:)

(q,K) is Element of the carrier of q

(q,(q,K)) is Element of the carrier of (q .:)

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

K is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of K is non empty set

a is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

a .: is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of a is non empty set

the L_meet of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) commutative associative idempotent Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]

[: the carrier of a, the carrier of a:] is non empty set

[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

the L_join of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) commutative associative idempotent Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]

LattStr(# the carrier of a, the L_meet of a, the L_join of a #) is non empty strict LattStr

the carrier of (a .:) is non empty set

c is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

c .: is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of c is non empty set

the L_meet of c is Relation-like [: the carrier of c, the carrier of c:] -defined the carrier of c -valued Function-like V18([: the carrier of c, the carrier of c:], the carrier of c) commutative associative idempotent Element of bool [:[: the carrier of c, the carrier of c:], the carrier of c:]

[: the carrier of c, the carrier of c:] is non empty set

[:[: the carrier of c, the carrier of c:], the carrier of c:] is non empty set

bool [:[: the carrier of c, the carrier of c:], the carrier of c:] is non empty set

the L_join of c is Relation-like [: the carrier of c, the carrier of c:] -defined the carrier of c -valued Function-like V18([: the carrier of c, the carrier of c:], the carrier of c) commutative associative idempotent Element of bool [:[: 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

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_meet of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the L_meet of L . (p,q) is Element of the carrier of L

[p,q] is set

{p,q} is non empty set

{p} is non empty set

{{p,q},{p}} is non empty set

the L_meet of L . [p,q] is set

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 [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative idempotent Element of bool [:[: 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,p) is Element of the carrier of (L .:)

the carrier of (L .:) is non empty set

(L,q) is Element of the carrier of (L .:)

(L,p) "\/" (L,q) is Element of the carrier of (L .:)

the L_join of (L .:) is Relation-like [: the carrier of (L .:), the carrier of (L .:):] -defined the carrier of (L .:) -valued Function-like V18([: the carrier of (L .:), the carrier of (L .:):], the carrier of (L .:)) commutative associative idempotent Element of bool [:[: the carrier of (L .:), the carrier of (L .:):], the carrier of (L .:):]

[: the carrier of (L .:), the carrier of (L .:):] is non empty set

[:[: the carrier of (L .:), the carrier of (L .:):], the carrier of (L .:):] is non empty set

bool [:[: the carrier of (L .:), the carrier of (L .:):], the carrier of (L .:):] is non empty set

the L_join of (L .:) . ((L,p),(L,q)) is Element of the carrier of (L .:)

[(L,p),(L,q)] is set

{(L,p),(L,q)} is non empty set