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

the carrier of Nat_Lattice is non empty set
bool K166() is non empty set
NATPLUS is non empty Element of bool K166()
is non empty set
is non 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,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:]

[: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
c9 is Element of L
c is Element of L
q . (c9,c) is Element of L
[c9,c] is set
{c9,c} is non empty set
{c9} is non empty set
{{c9,c},{c9}} is non empty set
q . [c9,c] is set
q . (c,c9) is Element of L
[c,c9] is set
{c,c9} is non empty set
{c} is non empty set
{{c,c9},{c}} is non empty set
q . [c,c9] is set
[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
c9 is Element of p
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,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

[: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,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,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
c9 is Element of p
b . (a9,c9) is Element of p
[a9,c9] is set
{a9,c9} is non empty set
{a9} is non empty set
{{a9,c9},{a9}} is non empty set
b . [a9,c9] is set
b9 . (a,(b . (a9,c9))) is Element of p
[a,(b . (a9,c9))] is set
{a,(b . (a9,c9))} is non empty set
{a} is non empty set
{{a,(b . (a9,c9))},{a}} is non empty set
b9 . [a,(b . (a9,c9))] is set
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,c9) is Element of p
[a,c9] is set
{a,c9} is non empty set
{{a,c9},{a}} is non empty set
b9 . [a,c9] is set
b . ((b9 . (a,a9)),(b9 . (a,c9))) is Element of p
[(b9 . (a,a9)),(b9 . (a,c9))] is set
{(b9 . (a,a9)),(b9 . (a,c9))} is non empty set
{(b9 . (a,a9))} is non empty set
{{(b9 . (a,a9)),(b9 . (a,c9))},{(b9 . (a,a9))}} is non empty set
b . [(b9 . (a,a9)),(b9 . (a,c9))] is set
b9 . (a,a9) is Element of p
b9 . (a,c9) is Element of p
b . (a9,c9) is Element of p
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,c9))] is Element of [:p,p:]
{a,(b . (a9,c9))} is non empty set
{{a,(b . (a9,c9))},{a}} is non empty set
q . [a,(b . (a9,c9))] is set
q . (a,(b . (a9,c9))) is set
[a,(b . (a9,c9))] is set
q . [a,(b . (a9,c9))] is 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,c9] is Element of [:p,p:]
b . [a9,c9] is set
K . [a9,c9] is set
[(b9 . (a,a9)),(b9 . (a,c9))] is Element of [:p,p:]
{(b9 . (a,a9)),(b9 . (a,c9))} is non empty set
{(b9 . (a,a9))} is non empty set
{{(b9 . (a,a9)),(b9 . (a,c9))},{(b9 . (a,a9))}} is non empty set
b . [(b9 . (a,a9)),(b9 . (a,c9))] is set
K . [(b9 . (a,a9)),(b9 . (a,c9))] is set
K . ((b9 . (a,a9)),(b9 . (a,c9))) is set
[(b9 . (a,a9)),(b9 . (a,c9))] is set
K . [(b9 . (a,a9)),(b9 . (a,c9))] is set

b9 . [a,(b . (a9,c9))] is set
[a,a9] is Element of [:p,p:]
b9 . [a,a9] is set
q . [a,a9] is set
[a,c9] is Element of [:p,p:]
b9 . [a,c9] is set
q . [a,c9] is set
b9 . (a,(b . (a9,c9))) is Element of p
b9 . [a,(b . (a9,c9))] is set
b . ((b9 . (a,a9)),(b9 . (a,c9))) is Element of p
b . [(b9 . (a,a9)),(b9 . (a,c9))] is set
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
c9 is Element of p
b9 . ((b . (a,a9)),c9) is Element of p
[(b . (a,a9)),c9] is set
{(b . (a,a9)),c9} is non empty set
{(b . (a,a9))} is non empty set
{{(b . (a,a9)),c9},{(b . (a,a9))}} is non empty set
b9 . [(b . (a,a9)),c9] is set
b9 . (a,c9) is Element of p
[a,c9] is set
{a,c9} is non empty set
{{a,c9},{a}} is non empty set
b9 . [a,c9] is set
b9 . (a9,c9) is Element of p
[a9,c9] is set
{a9,c9} is non empty set
{a9} is non empty set
{{a9,c9},{a9}} is non empty set
b9 . [a9,c9] is set
b . ((b9 . (a,c9)),(b9 . (a9,c9))) is Element of p
[(b9 . (a,c9)),(b9 . (a9,c9))] is set
{(b9 . (a,c9)),(b9 . (a9,c9))} is non empty set
{(b9 . (a,c9))} is non empty set
{{(b9 . (a,c9)),(b9 . (a9,c9))},{(b9 . (a,c9))}} is non empty set
b . [(b9 . (a,c9)),(b9 . (a9,c9))] is set
b . (a,a9) is Element of p
b9 . (a,c9) is Element of p
b9 . (a9,c9) is Element of p
[(b9 . (a,c9)),(b9 . (a9,c9))] is Element of [:p,p:]
{(b9 . (a,c9)),(b9 . (a9,c9))} is non empty set
{(b9 . (a,c9))} is non empty set
{{(b9 . (a,c9)),(b9 . (a9,c9))},{(b9 . (a,c9))}} is non empty set
K . [(b9 . (a,c9)),(b9 . (a9,c9))] is set
K . ((b9 . (a,c9)),(b9 . (a9,c9))) is set
[(b9 . (a,c9)),(b9 . (a9,c9))] is set
K . [(b9 . (a,c9)),(b9 . (a9,c9))] is 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)),c9] is Element of [:p,p:]
{(b . (a,a9)),c9} is non empty set
{(b . (a,a9))} is non empty set
{{(b . (a,a9)),c9},{(b . (a,a9))}} is non empty set
b9 . [(b . (a,a9)),c9] is set
q . [(b . (a,a9)),c9] is set

[a,a9] is Element of [:p,p:]
b . [a,a9] is set
K . [a,a9] is set
b . [(b9 . (a,c9)),(b9 . (a9,c9))] is set
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)),c9) is set
[(b . (a,a9)),c9] is set
q . [(b . (a,a9)),c9] is set
[a9,c9] is Element of [:p,p:]
b9 . [a9,c9] is set
q . [a9,c9] is set
[a,c9] is Element of [:p,p:]
b9 . [a,c9] is set
q . [a,c9] is set
b9 . ((b . (a,a9)),c9) is Element of p
b9 . [(b . (a,a9)),c9] is set
b . ((b9 . (a,c9)),(b9 . (a9,c9))) is Element of p
b . [(b9 . (a,c9)),(b9 . (a9,c9))] 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,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,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,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,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

[:p,p:] is Relation-like L -defined L -valued non empty Element of bool [:L,L:]
bool [:L,L:] is non empty 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

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

LattStr(# the carrier of p, the L_meet of p, the L_join of p #) is strict 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
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

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

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
() "/\" b9 is Element of the carrier of L
the L_meet of L . ((),b9) is Element of the carrier of L
[(),b9] is set
{(),b9} is non empty set
{()} is non empty set
{{(),b9},{()}} is non empty set
the L_meet of 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

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

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

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

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

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

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

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

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

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

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

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

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

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

the carrier of L is non empty set
p 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_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

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

the carrier of L is non empty set

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

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

the carrier of L is non empty set

the carrier of K is non empty set

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

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

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