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
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 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
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
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,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
dom b9 is Relation-like 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
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)),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
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,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 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