:: FILTER_0 semantic presentation

omega is set
bool omega is non empty set
{} is empty set
the empty set is empty set
1 is non empty set
L is non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr
the carrier of L is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
z is Element of the carrier of L
z "\/" x 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 V36([: 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_join of L . (z,x) is Element of the carrier of L
[z,x] is V33() set
{z,x} is non empty set
{z} is non empty set
{{z,x},{z}} is non empty set
the L_join of L . [z,x] is set
z "\/" y is Element of the carrier of L
the L_join of L . (z,y) is Element of the carrier of L
[z,y] is V33() set
{z,y} is non empty set
{{z,y},{z}} is non empty set
the L_join of L . [z,y] is set
x "\/" y is Element of the carrier of L
the L_join of L . (x,y) is Element of the carrier of L
[x,y] is V33() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the L_join of L . [x,y] is set
(z "\/" x) "\/" (z "\/" y) is Element of the carrier of L
the L_join of L . ((z "\/" x),(z "\/" y)) is Element of the carrier of L
[(z "\/" x),(z "\/" y)] is V33() set
{(z "\/" x),(z "\/" y)} is non empty set
{(z "\/" x)} is non empty set
{{(z "\/" x),(z "\/" y)},{(z "\/" x)}} is non empty set
the L_join of L . [(z "\/" x),(z "\/" y)] is set
z "\/" (z "\/" x) is Element of the carrier of L
the L_join of L . (z,(z "\/" x)) is Element of the carrier of L
[z,(z "\/" x)] is V33() set
{z,(z "\/" x)} is non empty set
{{z,(z "\/" x)},{z}} is non empty set
the L_join of L . [z,(z "\/" x)] is set
(z "\/" (z "\/" x)) "\/" y is Element of the carrier of L
the L_join of L . ((z "\/" (z "\/" x)),y) is Element of the carrier of L
[(z "\/" (z "\/" x)),y] is V33() set
{(z "\/" (z "\/" x)),y} is non empty set
{(z "\/" (z "\/" x))} is non empty set
{{(z "\/" (z "\/" x)),y},{(z "\/" (z "\/" x))}} is non empty set
the L_join of L . [(z "\/" (z "\/" x)),y] is set
z "\/" z is Element of the carrier of L
the L_join of L . (z,z) is Element of the carrier of L
[z,z] is V33() set
{z,z} is non empty set
{{z,z},{z}} is non empty set
the L_join of L . [z,z] is set
(z "\/" z) "\/" x is Element of the carrier of L
the L_join of L . ((z "\/" z),x) is Element of the carrier of L
[(z "\/" z),x] is V33() set
{(z "\/" z),x} is non empty set
{(z "\/" z)} is non empty set
{{(z "\/" z),x},{(z "\/" z)}} is non empty set
the L_join of L . [(z "\/" z),x] is set
((z "\/" z) "\/" x) "\/" y is Element of the carrier of L
the L_join of L . (((z "\/" z) "\/" x),y) is Element of the carrier of L
[((z "\/" z) "\/" x),y] is V33() set
{((z "\/" z) "\/" x),y} is non empty set
{((z "\/" z) "\/" x)} is non empty set
{{((z "\/" z) "\/" x),y},{((z "\/" z) "\/" x)}} is non empty set
the L_join of L . [((z "\/" z) "\/" x),y] is set
(z "\/" x) "\/" y is Element of the carrier of L
the L_join of L . ((z "\/" x),y) is Element of the carrier of L
[(z "\/" x),y] is V33() set
{(z "\/" x),y} is non empty set
{{(z "\/" x),y},{(z "\/" x)}} is non empty set
the L_join of L . [(z "\/" x),y] 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
x is Element of the carrier of L
y is Element of the carrier of L
z is Element of the carrier of L
x "/\" z 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 V36([: 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 . (x,z) is Element of the carrier of L
[x,z] is V33() set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
the L_meet of L . [x,z] is set
y "/\" z is Element of the carrier of L
the L_meet of L . (y,z) is Element of the carrier of L
[y,z] is V33() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the L_meet of L . [y,z] 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
x is Element of the carrier of L
y is Element of the carrier of L
z is Element of the carrier of L
z "\/" y 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 V36([: 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_join of L . (z,y) is Element of the carrier of L
[z,y] is V33() set
{z,y} is non empty set
{z} is non empty set
{{z,y},{z}} is non empty set
the L_join of L . [z,y] is set
x "\/" z is Element of the carrier of L
the L_join of L . (x,z) is Element of the carrier of L
[x,z] is V33() set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
the L_join of L . [x,z] is set
y "\/" z is Element of the carrier of L
the L_join of L . (y,z) is Element of the carrier of L
[y,z] is V33() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the L_join of L . [y,z] is set
L is non empty join-commutative join-associative join-absorbing LattStr
the carrier of L is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
z is Element of the carrier of L
j is Element of the carrier of L
x "\/" z 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 V36([: 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_join of L . (x,z) is Element of the carrier of L
[x,z] is V33() set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
the L_join of L . [x,z] is set
y "\/" j is Element of the carrier of L
the L_join of L . (y,j) is Element of the carrier of L
[y,j] is V33() set
{y,j} is non empty set
{y} is non empty set
{{y,j},{y}} is non empty set
the L_join of L . [y,j] is set
x "\/" y is Element of the carrier of L
the L_join of L . (x,y) is Element of the carrier of L
[x,y] is V33() set
{x,y} is non empty set
{{x,y},{x}} is non empty set
the L_join of L . [x,y] is set
z "\/" j is Element of the carrier of L
the L_join of L . (z,j) is Element of the carrier of L
[z,j] is V33() set
{z,j} is non empty set
{z} is non empty set
{{z,j},{z}} is non empty set
the L_join of L . [z,j] is set
(x "\/" y) "\/" (z "\/" j) is Element of the carrier of L
the L_join of L . ((x "\/" y),(z "\/" j)) is Element of the carrier of L
[(x "\/" y),(z "\/" j)] is V33() set
{(x "\/" y),(z "\/" j)} is non empty set
{(x "\/" y)} is non empty set
{{(x "\/" y),(z "\/" j)},{(x "\/" y)}} is non empty set
the L_join of L . [(x "\/" y),(z "\/" j)] is set
y "\/" x is Element of the carrier of L
the L_join of L . (y,x) is Element of the carrier of L
[y,x] is V33() set
{y,x} is non empty set
{{y,x},{y}} is non empty set
the L_join of L . [y,x] is set
(y "\/" x) "\/" z is Element of the carrier of L
the L_join of L . ((y "\/" x),z) is Element of the carrier of L
[(y "\/" x),z] is V33() set
{(y "\/" x),z} is non empty set
{(y "\/" x)} is non empty set
{{(y "\/" x),z},{(y "\/" x)}} is non empty set
the L_join of L . [(y "\/" x),z] is set
((y "\/" x) "\/" z) "\/" j is Element of the carrier of L
the L_join of L . (((y "\/" x) "\/" z),j) is Element of the carrier of L
[((y "\/" x) "\/" z),j] is V33() set
{((y "\/" x) "\/" z),j} is non empty set
{((y "\/" x) "\/" z)} is non empty set
{{((y "\/" x) "\/" z),j},{((y "\/" x) "\/" z)}} is non empty set
the L_join of L . [((y "\/" x) "\/" z),j] is set
y "\/" (x "\/" z) is Element of the carrier of L
the L_join of L . (y,(x "\/" z)) is Element of the carrier of L
[y,(x "\/" z)] is V33() set
{y,(x "\/" z)} is non empty set
{{y,(x "\/" z)},{y}} is non empty set
the L_join of L . [y,(x "\/" z)] is set
(y "\/" (x "\/" z)) "\/" j is Element of the carrier of L
the L_join of L . ((y "\/" (x "\/" z)),j) is Element of the carrier of L
[(y "\/" (x "\/" z)),j] is V33() set
{(y "\/" (x "\/" z)),j} is non empty set
{(y "\/" (x "\/" z))} is non empty set
{{(y "\/" (x "\/" z)),j},{(y "\/" (x "\/" z))}} is non empty set
the L_join of L . [(y "\/" (x "\/" z)),j] is set
(x "\/" z) "\/" (y "\/" j) is Element of the carrier of L
the L_join of L . ((x "\/" z),(y "\/" j)) is Element of the carrier of L
[(x "\/" z),(y "\/" j)] is V33() set
{(x "\/" z),(y "\/" j)} is non empty set
{(x "\/" z)} is non empty set
{{(x "\/" z),(y "\/" j)},{(x "\/" z)}} is non empty set
the L_join of L . [(x "\/" z),(y "\/" j)] is set
L is non empty meet-commutative meet-associative meet-absorbing join-absorbing LattStr
the carrier of L is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
z is Element of the carrier of L
j is Element of the carrier of L
x "/\" z 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 V36([: 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 . (x,z) is Element of the carrier of L
[x,z] is V33() set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
the L_meet of L . [x,z] is set
y "/\" j is Element of the carrier of L
the L_meet of L . (y,j) is Element of the carrier of L
[y,j] is V33() set
{y,j} is non empty set
{y} is non empty set
{{y,j},{y}} is non empty set
the L_meet of L . [y,j] is set
x "/\" y is Element of the carrier of L
the L_meet of L . (x,y) is Element of the carrier of L
[x,y] is V33() set
{x,y} is non empty set
{{x,y},{x}} is non empty set
the L_meet of L . [x,y] is set
z "/\" j is Element of the carrier of L
the L_meet of L . (z,j) is Element of the carrier of L
[z,j] is V33() set
{z,j} is non empty set
{z} is non empty set
{{z,j},{z}} is non empty set
the L_meet of L . [z,j] is set
(x "/\" y) "/\" (z "/\" j) is Element of the carrier of L
the L_meet of L . ((x "/\" y),(z "/\" j)) is Element of the carrier of L
[(x "/\" y),(z "/\" j)] is V33() set
{(x "/\" y),(z "/\" j)} is non empty set
{(x "/\" y)} is non empty set
{{(x "/\" y),(z "/\" j)},{(x "/\" y)}} is non empty set
the L_meet of L . [(x "/\" y),(z "/\" j)] is set
(x "/\" y) "/\" z is Element of the carrier of L
the L_meet of L . ((x "/\" y),z) is Element of the carrier of L
[(x "/\" y),z] is V33() set
{(x "/\" y),z} is non empty set
{{(x "/\" y),z},{(x "/\" y)}} is non empty set
the L_meet of L . [(x "/\" y),z] is set
((x "/\" y) "/\" z) "/\" j is Element of the carrier of L
the L_meet of L . (((x "/\" y) "/\" z),j) is Element of the carrier of L
[((x "/\" y) "/\" z),j] is V33() set
{((x "/\" y) "/\" z),j} is non empty set
{((x "/\" y) "/\" z)} is non empty set
{{((x "/\" y) "/\" z),j},{((x "/\" y) "/\" z)}} is non empty set
the L_meet of L . [((x "/\" y) "/\" z),j] is set
y "/\" (x "/\" z) is Element of the carrier of L
the L_meet of L . (y,(x "/\" z)) is Element of the carrier of L
[y,(x "/\" z)] is V33() set
{y,(x "/\" z)} is non empty set
{{y,(x "/\" z)},{y}} is non empty set
the L_meet of L . [y,(x "/\" z)] is set
(y "/\" (x "/\" z)) "/\" j is Element of the carrier of L
the L_meet of L . ((y "/\" (x "/\" z)),j) is Element of the carrier of L
[(y "/\" (x "/\" z)),j] is V33() set
{(y "/\" (x "/\" z)),j} is non empty set
{(y "/\" (x "/\" z))} is non empty set
{{(y "/\" (x "/\" z)),j},{(y "/\" (x "/\" z))}} is non empty set
the L_meet of L . [(y "/\" (x "/\" z)),j] is set
(x "/\" z) "/\" (y "/\" j) is Element of the carrier of L
the L_meet of L . ((x "/\" z),(y "/\" j)) is Element of the carrier of L
[(x "/\" z),(y "/\" j)] is V33() set
{(x "/\" z),(y "/\" j)} is non empty set
{(x "/\" z)} is non empty set
{{(x "/\" z),(y "/\" j)},{(x "/\" z)}} is non empty set
the L_meet of L . [(x "/\" z),(y "/\" j)] is set
L is non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr
the carrier of L is non empty set
x is Element of the carrier of L
z is Element of the carrier of L
y is Element of the carrier of L
x "\/" y 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 V36([: 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_join of L . (x,y) is Element of the carrier of L
[x,y] is V33() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the L_join of L . [x,y] is set
z "\/" z is Element of the carrier of L
the L_join of L . (z,z) is Element of the carrier of L
[z,z] is V33() set
{z,z} is non empty set
{z} is non empty set
{{z,z},{z}} is non empty set
the L_join of L . [z,z] is set
L is non empty meet-commutative meet-associative meet-absorbing join-absorbing LattStr
the carrier of L is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
z is Element of the carrier of L
y "/\" z 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 V36([: 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 . (y,z) is Element of the carrier of L
[y,z] is V33() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the L_meet of L . [y,z] is set
x "/\" x is Element of the carrier of L
the L_meet of L . (x,x) is Element of the carrier of L
[x,x] is V33() set
{x,x} is non empty set
{x} is non empty set
{{x,x},{x}} is non empty set
the L_meet of L . [x,x] 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
x is non empty Element of bool the carrier of L
y is Element of the carrier of L
z is Element of the carrier of L
y "/\" z 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 V36([: 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 . (y,z) is Element of the carrier of L
[y,z] is V33() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the L_meet of L . [y,z] is set
y is Element of the carrier of L
z is Element of the carrier of L
y "/\" z 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 V36([: 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 . (y,z) is Element of the carrier of L
[y,z] is V33() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the L_meet of L . [y,z] 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
x is non empty Element of bool the carrier of L
y is Element of the carrier of L
z is Element of the carrier of L
y "/\" z 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 V36([: 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 . (y,z) is Element of the carrier of L
[y,z] is V33() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the L_meet of L . [y,z] is set
j is Element of the carrier of L
k is Element of the carrier of L
y is Element of the carrier of L
z 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
bool the carrier of L is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
x "\/" y 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 V36([: 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_join of L . (x,y) is Element of the carrier of L
[x,y] is V33() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the L_join of L . [x,y] is set
y "\/" x is Element of the carrier of L
the L_join of L . (y,x) is Element of the carrier of L
[y,x] is V33() set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
the L_join of L . [y,x] is set
z 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
bool the carrier of L is non empty set
Top L is Element of the carrier of L
x is non empty final meet-closed join-closed Element of bool the carrier of L
y is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of y is non empty set
z is Element of the carrier of y
Top y is Element of the carrier of y
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
Top L is Element of the carrier of L
{(Top L)} is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
x is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of x is non empty set
y is Element of the carrier of x
Top x is Element of the carrier of x
z is Element of the carrier of x
{(Top x)} is non empty Element of bool the carrier of x
bool the carrier of x is non empty set
y "/\" z is Element of the carrier of x
the L_meet of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V36([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the L_meet of x . (y,z) is Element of the carrier of x
[y,z] is V33() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the L_meet of x . [y,z] is set
z "/\" y is Element of the carrier of x
the L_meet of x . (z,y) is Element of the carrier of x
[z,y] is V33() set
{z,y} is non empty set
{z} is non empty set
{{z,y},{z}} is non empty set
the L_meet of x . [z,y] 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
x is Element of the carrier of L
{x} is non empty Element of bool the carrier of L
z is Element of the carrier of L
x "\/" z 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 V36([: 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_join of L . (x,z) is Element of the carrier of L
[x,z] is V33() set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
the L_join of L . [x,z] is set
z "\/" x is Element of the carrier of L
the L_join of L . (z,x) is Element of the carrier of L
[z,x] is V33() set
{z,x} is non empty set
{z} is non empty set
{{z,x},{z}} is non empty set
the L_join of L . [z,x] is set
y is non empty final meet-closed join-closed Element of bool the carrier of L
x "\/" z 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
bool the carrier of L is non empty set
[#] L is non empty non proper V82(L) 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
bool 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
the carrier of L is non empty set
x is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : x [= b₁ } is set
bool the carrier of L is non empty set
z is non empty set
j is set
k is Element of the carrier of L
k is Element of the carrier of L
j is non empty Element of bool the carrier of L
x "/\" x 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 V36([: 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 . (x,x) is Element of the carrier of L
[x,x] is V33() set
{x,x} is non empty set
{x} is non empty set
{{x,x},{x}} is non empty set
the L_meet of L . [x,x] is set
k "/\" x is Element of the carrier of L
the L_meet of L . (k,x) is Element of the carrier of L
[k,x] is V33() set
{k,x} is non empty set
{k} is non empty set
{{k,x},{k}} is non empty set
the L_meet of L . [k,x] is set
a is Element of the carrier of L
FI is Element of the carrier of L
x "/\" k is Element of the carrier of L
the L_meet of L . (x,k) is Element of the carrier of L
[x,k] is V33() set
{x,k} is non empty set
{{x,k},{x}} is non empty set
the L_meet of L . [x,k] is set
FI "/\" k is Element of the carrier of L
the L_meet of L . (FI,k) is Element of the carrier of L
[FI,k] is V33() set
{FI,k} is non empty set
{FI} is non empty set
{{FI,k},{FI}} is non empty set
the L_meet of L . [FI,k] is set
a is Element of the carrier of L
k "/\" FI is Element of the carrier of L
the L_meet of L . (k,FI) is Element of the carrier of L
[k,FI] is V33() set
{k,FI} is non empty set
{{k,FI},{k}} is non empty set
the L_meet of L . [k,FI] is set
k is Element of the carrier of L
FI is Element of the carrier of L
a 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
x is Element of the carrier of L
y is Element of the carrier of L
(L,y) is non empty final meet-closed join-closed Element of bool the carrier of L
bool the carrier of L is non empty set
{ b₁ where b₁ is Element of the carrier of L : y [= b₁ } is set
z is Element of the carrier of L
z 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
x is Element of the carrier of L
(L,x) is non empty final meet-closed join-closed Element of bool the carrier of L
bool the carrier of L is non empty set
{ b₁ where b₁ is Element of the carrier of L : x [= b₁ } is set
y is Element of the carrier of L
x "\/" y 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 V36([: 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_join of L . (x,y) is Element of the carrier of L
[x,y] is V33() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the L_join of L . [x,y] is set
y "\/" x is Element of the carrier of L
the L_join of L . (y,x) is Element of the carrier of L
[y,x] is V33() set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
the L_join of L . [y,x] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(L) is non empty final meet-closed join-closed Element of bool the carrier of L
the carrier of L is non empty set
bool the carrier of L is non empty set
Bottom L is Element of the carrier of L
(L,(Bottom L)) is non empty final meet-closed join-closed Element of bool the carrier of L
{ b₁ where b₁ is Element of the carrier of L : Bottom L [= b₁ } is set
y is set
x is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of x is non empty set
z is Element of the carrier of x
Bottom x is Element of the carrier of x
z "/\" (Bottom x) is Element of the carrier of x
the L_meet of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V36([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the L_meet of x . (z,(Bottom x)) is Element of the carrier of x
[z,(Bottom x)] is V33() set
{z,(Bottom x)} is non empty set
{z} is non empty set
{{z,(Bottom x)},{z}} is non empty set
the L_meet of x . [z,(Bottom x)] 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
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
x is Element of the carrier of L
y is non empty final meet-closed join-closed Element of bool the carrier of L
z is set
j is Element of the carrier of L
x "/\" j 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 V36([: 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 . (x,j) is Element of the carrier of L
[x,j] is V33() set
{x,j} is non empty set
{x} is non empty set
{{x,j},{x}} is non empty set
the L_meet of L . [x,j] is set
y is non empty final meet-closed join-closed Element of bool the carrier of L
{ b₁ where b₁ is Element of bool the carrier of L : ( y c= b₁ & b₁ is non empty final meet-closed join-closed Element of bool the carrier of L & not b₁ = the carrier of L ) } is set
j is set
k is Element of bool the carrier of L
j is set
k is Element of bool the carrier of L
the Element of y is Element of y
k is set
{y} is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
k \/ {y} is non empty set
union (k \/ {y}) is set
FI is set
a is non empty set
b is set
c is set
c is Element of the carrier of L
b is non empty Element of bool the carrier of L
j is Element of the carrier of L
c "/\" j 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 V36([: 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 . (c,j) is Element of the carrier of L
[c,j] is V33() set
{c,j} is non empty set
{c} is non empty set
{{c,j},{c}} is non empty set
the L_meet of L . [c,j] is set
r9 is set
s9 is set
r9 is set
c is non empty final meet-closed join-closed Element of bool the carrier of L
j is set
r9 is Element of bool the carrier of L
j is set
j is set
j is set
k is Element of bool the carrier of L
FI is non empty final meet-closed join-closed Element of bool the carrier of L
a 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
x is Element of the carrier of L
(L,x) is non empty final meet-closed join-closed Element of bool the carrier of L
bool the carrier of L is non empty set
{ b₁ where b₁ is Element of the carrier of L : x [= b₁ } is set
y is Element of the carrier of L
x "/\" y 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 V36([: 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 . (x,y) is Element of the carrier of L
[x,y] is V33() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the L_meet of L . [x,y] 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
Bottom L is Element of the carrier of L
bool the carrier of L is non empty set
x is Element of the carrier of L
y is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of y is non empty set
z is Element of the carrier of y
Bottom y is Element of the carrier of y
z "/\" (Bottom y) is Element of the carrier of y
the L_meet of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like V36([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the L_meet of y . (z,(Bottom y)) is Element of the carrier of y
[z,(Bottom y)] is V33() set
{z,(Bottom y)} is non empty set
{z} is non empty set
{{z,(Bottom y)},{z}} is non empty set
the L_meet of y . [z,(Bottom y)] is set
(L,x) is non empty final meet-closed join-closed Element of bool the carrier of L
{ b₁ where b₁ is Element of the carrier of L : x [= b₁ } is set
j 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
bool the carrier of L is non empty set
x is non empty Element of bool the carrier of L
the Element of x is Element of x
bool the carrier of L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
z is set
(L) is non empty final meet-closed join-closed Element of bool the carrier of L
k is set
j is Element of the carrier of L
meet z is set
k is non empty set
FI is set
a is Element of the carrier of L
FI is non empty Element of bool the carrier of L
b is Element of the carrier of L
a "/\" b 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 V36([: 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 . (a,b) is Element of the carrier of L
[a,b] is V33() set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
the L_meet of L . [a,b] is set
c is set
j is non empty final meet-closed join-closed Element of bool the carrier of L
c is set
j is non empty final meet-closed join-closed Element of bool the carrier of L
c is set
j is non empty final meet-closed join-closed Element of bool the carrier of L
a is non empty final meet-closed join-closed Element of bool the carrier of L
b is set
b is non empty final meet-closed join-closed Element of bool the carrier of L
y is non empty final meet-closed join-closed Element of bool the carrier of L
z 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
bool the carrier of L is non empty set
x is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x) is non empty final meet-closed join-closed Element of bool the carrier of L
y 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
bool the carrier of L is non empty set
x is non empty Element of bool the carrier of L
(L,x) is non empty final meet-closed join-closed Element of bool the carrier of L
y is non empty Element of bool the carrier of L
(L,y) 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
bool the carrier of L is non empty set
x is Element of the carrier of L
(L,x) is non empty final meet-closed join-closed Element of bool the carrier of L
{ b₁ where b₁ is Element of the carrier of L : x [= b₁ } is set
y is non empty Element of bool the carrier of L
(L,y) is non empty final meet-closed join-closed Element of bool the carrier of L
z is set
j 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
bool the carrier of L is non empty set
x is Element of the carrier of L
{x} is non empty Element of bool the carrier of L
(L,x) is non empty final meet-closed join-closed Element of bool the carrier of L
{ b₁ where b₁ is Element of the carrier of L : x [= b₁ } is set
y is non empty Element of bool the carrier of L
(L,y) is non empty final meet-closed join-closed Element of bool the carrier of L
z 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
Bottom L is Element of the carrier of L
(L) is non empty final meet-closed join-closed Element of bool the carrier of L
x is non empty Element of bool the carrier of L
(L,x) is non empty final meet-closed join-closed Element of bool the carrier of L
(L,(Bottom L)) is non empty final meet-closed join-closed Element of bool the carrier of L
{ b₁ where b₁ is Element of the carrier of L : Bottom L [= b₁ } 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
Bottom L is Element of the carrier of L
(L) is non empty final meet-closed join-closed Element of bool the carrier of L
x is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x) 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
bool 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
the carrier of L is non empty set
x 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 LattStr
j is Element of the carrier of L
j ` is Element of the carrier of L
k is Element of the carrier of L
(j `) "\/" 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 V36([: 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_join of L . ((j `),k) is Element of the carrier of L
[(j `),k] is V33() set
{(j `),k} is non empty set
{(j `)} is non empty set
{{(j `),k},{(j `)}} is non empty set
the L_join of L . [(j `),k] is set
j "/\" ((j `) "\/" 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 V36([: 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 L_meet of L . (j,((j `) "\/" k)) is Element of the carrier of L
[j,((j `) "\/" k)] is V33() set
{j,((j `) "\/" k)} is non empty set
{j} is non empty set
{{j,((j `) "\/" k)},{j}} is non empty set
the L_meet of L . [j,((j `) "\/" k)] is set
z is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of z is non empty set
the carrier of x is non empty set
c is Element of the carrier of x
c ` is Element of the carrier of x
c "/\" (c `) is Element of the carrier of x
the L_meet of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V36([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the L_meet of x . (c,(c `)) is Element of the carrier of x
[c,(c `)] is V33() set
{c,(c `)} is non empty set
{c} is non empty set
{{c,(c `)},{c}} is non empty set
the L_meet of x . [c,(c `)] is set
Bottom L is Element of the carrier of L
Bottom z is Element of the carrier of z
a is Element of the carrier of z
b is Element of the carrier of z
a "/\" b is Element of the carrier of z
the L_meet of z is Relation-like [: the carrier of z, the carrier of z:] -defined the carrier of z -valued Function-like V36([: the carrier of z, the carrier of z:], the carrier of z) Element of bool [:[: the carrier of z, the carrier of z:], the carrier of z:]
[: the carrier of z, the carrier of z:] is non empty set
[:[: the carrier of z, the carrier of z:], the carrier of z:] is non empty set
bool [:[: the carrier of z, the carrier of z:], the carrier of z:] is non empty set
the L_meet of z . (a,b) is Element of the carrier of z
[a,b] is V33() set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
the L_meet of z . [a,b] is set
(Bottom z) "\/" (a "/\" b) is Element of the carrier of z
the L_join of z is Relation-like [: the carrier of z, the carrier of z:] -defined the carrier of z -valued Function-like V36([: the carrier of z, the carrier of z:], the carrier of z) Element of bool [:[: the carrier of z, the carrier of z:], the carrier of z:]
the L_join of z . ((Bottom z),(a "/\" b)) is Element of the carrier of z
[(Bottom z),(a "/\" b)] is V33() set
{(Bottom z),(a "/\" b)} is non empty set
{(Bottom z)} is non empty set
{{(Bottom z),(a "/\" b)},{(Bottom z)}} is non empty set
the L_join of z . [(Bottom z),(a "/\" b)] is set
j is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of j is non empty set
r9 is Element of the carrier of j
s is Element of the carrier of j
r9 "/\" s is Element of the carrier of j
the L_meet of j is Relation-like [: the carrier of j, the carrier of j:] -defined the carrier of j -valued Function-like V36([: the carrier of j, the carrier of j:], the carrier of j) Element of bool [:[: the carrier of j, the carrier of j:], the carrier of j:]
[: the carrier of j, the carrier of j:] is non empty set
[:[: the carrier of j, the carrier of j:], the carrier of j:] is non empty set
bool [:[: the carrier of j, the carrier of j:], the carrier of j:] is non empty set
the L_meet of j . (r9,s) is Element of the carrier of j
[r9,s] is V33() set
{r9,s} is non empty set
{r9} is non empty set
{{r9,s},{r9}} is non empty set
the L_meet of j . [r9,s] is set
r9 ` is Element of the carrier of j
r9 "/\" (r9 `) is Element of the carrier of j
the L_meet of j . (r9,(r9 `)) is Element of the carrier of j
[r9,(r9 `)] is V33() set
{r9,(r9 `)} is non empty set
{{r9,(r9 `)},{r9}} is non empty set
the L_meet of j . [r9,(r9 `)] is set
s9 is Element of the carrier of j
r9 "/\" s9 is Element of the carrier of j
the L_meet of j . (r9,s9) is Element of the carrier of j
[r9,s9] is V33() set
{r9,s9} is non empty set
{{r9,s9},{r9}} is non empty set
the L_meet of j . [r9,s9] is set
(r9 "/\" (r9 `)) "\/" (r9 "/\" s9) is Element of the carrier of j
the L_join of j is Relation-like [: the carrier of j, the carrier of j:] -defined the carrier of j -valued Function-like V36([: the carrier of j, the carrier of j:], the carrier of j) Element of bool [:[: the carrier of j, the carrier of j:], the carrier of j:]
the L_join of j . ((r9 "/\" (r9 `)),(r9 "/\" s9)) is Element of the carrier of j
[(r9 "/\" (r9 `)),(r9 "/\" s9)] is V33() set
{(r9 "/\" (r9 `)),(r9 "/\" s9)} is non empty set
{(r9 "/\" (r9 `))} is non empty set
{{(r9 "/\" (r9 `)),(r9 "/\" s9)},{(r9 "/\" (r9 `))}} is non empty set
the L_join of j . [(r9 "/\" (r9 `)),(r9 "/\" s9)] is set
r1 is Element of the carrier of L
j "/\" r1 is Element of the carrier of L
the L_meet of L . (j,r1) is Element of the carrier of L
[j,r1] is V33() set
{j,r1} is non empty set
{{j,r1},{j}} is non empty set
the L_meet of L . [j,r1] is set
y is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of y is non empty set
(c `) "\/" c is Element of the carrier of x
the L_join of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V36([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
the L_join of x . ((c `),c) is Element of the carrier of x
[(c `),c] is V33() set
{(c `),c} is non empty set
{(c `)} is non empty set
{{(c `),c},{(c `)}} is non empty set
the L_join of x . [(c `),c] is set
Top L is Element of the carrier of L
Top y is Element of the carrier of y
pp is Element of the carrier of y
pp ` is Element of the carrier of y
r99 is Element of the carrier of y
(pp `) "\/" r99 is Element of the carrier of y
the L_join of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like V36([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the L_join of y . ((pp `),r99) is Element of the carrier of y
[(pp `),r99] is V33() set
{(pp `),r99} is non empty set
{(pp `)} is non empty set
{{(pp `),r99},{(pp `)}} is non empty set
the L_join of y . [(pp `),r99] is set
(Top y) "/\" ((pp `) "\/" r99) is Element of the carrier of y
the L_meet of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like V36([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
the L_meet of y . ((Top y),((pp `) "\/" r99)) is Element of the carrier of y
[(Top y),((pp `) "\/" r99)] is V33() set
{(Top y),((pp `) "\/" r99)} is non empty set
{(Top y)} is non empty set
{{(Top y),((pp `) "\/" r99)},{(Top y)}} is non empty set
the L_meet of y . [(Top y),((pp `) "\/" r99)] is set
(j `) "\/" (j "/\" r1) is Element of the carrier of L
the L_join of L . ((j `),(j "/\" r1)) is Element of the carrier of L
[(j `),(j "/\" r1)] is V33() set
{(j `),(j "/\" r1)} is non empty set
{{(j `),(j "/\" r1)},{(j `)}} is non empty set
the L_join of L . [(j `),(j "/\" r1)] is set
r19 is Element of the carrier of j
r9 "/\" r19 is Element of the carrier of j
the L_meet of j . (r9,r19) is Element of the carrier of j
[r9,r19] is V33() set
{r9,r19} is non empty set
{{r9,r19},{r9}} is non empty set
the L_meet of j . [r9,r19] is set
(r9 `) "\/" (r9 "/\" r19) is Element of the carrier of j
the L_join of j . ((r9 `),(r9 "/\" r19)) is Element of the carrier of j
[(r9 `),(r9 "/\" r19)] is V33() set
{(r9 `),(r9 "/\" r19)} is non empty set
{(r9 `)} is non empty set
{{(r9 `),(r9 "/\" r19)},{(r9 `)}} is non empty set
the L_join of j . [(r9 `),(r9 "/\" r19)] is set
(r9 `) "\/" r9 is Element of the carrier of j
the L_join of j . ((r9 `),r9) is Element of the carrier of j
[(r9 `),r9] is V33() set
{(r9 `),r9} is non empty set
{{(r9 `),r9},{(r9 `)}} is non empty set
the L_join of j . [(r9 `),r9] is set
(r9 `) "\/" r19 is Element of the carrier of j
the L_join of j . ((r9 `),r19) is Element of the carrier of j
[(r9 `),r19] is V33() set
{(r9 `),r19} is non empty set
{{(r9 `),r19},{(r9 `)}} is non empty set
the L_join of j . [(r9 `),r19] is set
((r9 `) "\/" r9) "/\" ((r9 `) "\/" r19) is Element of the carrier of j
the L_meet of j . (((r9 `) "\/" r9),((r9 `) "\/" r19)) is Element of the carrier of j
[((r9 `) "\/" r9),((r9 `) "\/" r19)] is V33() set
{((r9 `) "\/" r9),((r9 `) "\/" r19)} is non empty set
{((r9 `) "\/" r9)} is non empty set
{{((r9 `) "\/" r9),((r9 `) "\/" r19)},{((r9 `) "\/" r9)}} is non empty set
the L_meet of j . [((r9 `) "\/" r9),((r9 `) "\/" r19)] is set
r1 "\/" (j `) is Element of the carrier of L
the L_join of L . (r1,(j `)) is Element of the carrier of L
[r1,(j `)] is V33() set
{r1,(j `)} is non empty set
{r1} is non empty set
{{r1,(j `)},{r1}} is non empty set
the L_join of L . [r1,(j `)] is set
the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr
the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr is non empty set
x is Element of the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr
x ` is Element of the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr
y is Element of the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr
(x `) "\/" y is Element of the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr
the L_join of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr is Relation-like [: the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr , the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr :] -defined the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr -valued Function-like V36([: the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr , the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr :], the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr ) Element of bool [:[: the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr , the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr :], the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr :]
[: the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr , the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr :] is non empty set
[:[: the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr , the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr :], the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr :] is non empty set
bool [:[: the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr , the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr :], the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr :] is non empty set
the L_join of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr . ((x `),y) is Element of the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr
[(x `),y] is V33() set
{(x `),y} is non empty set
{(x `)} is non empty set
{{(x `),y},{(x `)}} is non empty set
the L_join of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr . [(x `),y] is set
z is Element of the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr
j is Element of the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr
x "/\" j is Element of the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr
the L_meet of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr is Relation-like [: the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr , the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr :] -defined the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr -valued Function-like V36([: the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr , the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr :], the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr ) Element of bool [:[: the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr , the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr :], the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr :]
the L_meet of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr . (x,j) is Element of the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr
[x,j] is V33() set
{x,j} is non empty set
{x} is non empty set
{{x,j},{x}} is non empty set
the L_meet of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr . [x,j] is set
k is Element of the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr
x "/\" k is Element of the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr
the L_meet of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr . (x,k) is Element of the carrier of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr
[x,k] is V33() set
{x,k} is non empty set
{{x,k},{x}} is non empty set
the L_meet of the non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr . [x,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
x is Element of the carrier of L
y is Element of the carrier of L
z is Element of the carrier of L
x "/\" z 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 V36([: 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 . (x,z) is Element of the carrier of L
[x,z] is V33() set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
the L_meet of L . [x,z] is set
j is Element of the carrier of L
x "/\" j is Element of the carrier of L
the L_meet of L . (x,j) is Element of the carrier of L
[x,j] is V33() set
{x,j} is non empty set
{{x,j},{x}} is non empty set
the L_meet of L . [x,j] 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 Element of the carrier of L is Element of the carrier of L
(L, the Element of the carrier of L, the Element of the carrier of L) is Element of the carrier of L
y is Element of the carrier of L
z is Element of the carrier of L
y "\/" z 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 V36([: 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_join of L . (y,z) is Element of the carrier of L
[y,z] is V33() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the L_join of L . [y,z] is set
z "\/" y is Element of the carrier of L
the L_join of L . (z,y) is Element of the carrier of L
[z,y] is V33() set
{z,y} is non empty set
{z} is non empty set
{{z,y},{z}} is non empty set
the L_join of L . [z,y] is set
the Element of the carrier of L "/\" z 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 V36([: 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 L_meet of L . ( the Element of the carrier of L,z) is Element of the carrier of L
[ the Element of the carrier of L,z] is V33() set
{ the Element of the carrier of L,z} is non empty set
{ the Element of the carrier of L} is non empty set
{{ the Element of the carrier of L,z},{ the Element of the carrier of L}} is non empty set
the L_meet of L . [ the Element of the carrier of L,z] is set
z "\/" y is Element of the carrier of L
y "\/" z is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded () LattStr
the carrier of L is non empty set
Top L is Element of the carrier of L
x is Element of the carrier of L
(L,x,x) is Element of the carrier of L
y is Element of the carrier of L
x "/\" y 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 V36([: 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 . (x,y) is Element of the carrier of L
[x,y] is V33() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the L_meet of L . [x,y] is set
y "\/" (L,x,x) 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 V36([: 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 L_join of L . (y,(L,x,x)) is Element of the carrier of L
[y,(L,x,x)] is V33() set
{y,(L,x,x)} is non empty set
{y} is non empty set
{{y,(L,x,x)},{y}} is non empty set
the L_join of L . [y,(L,x,x)] 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
x is Element of the carrier of L
y is Element of the carrier of L
x "/\" y 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 V36([: 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 . (x,y) is Element of the carrier of L
[x,y] is V33() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the L_meet of L . [x,y] is set
z is Element of the carrier of L
y "\/" z 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 V36([: 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 L_join of L . (y,z) is Element of the carrier of L
[y,z] is V33() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the L_join of L . [y,z] is set
x "/\" (y "\/" z) is Element of the carrier of L
the L_meet of L . (x,(y "\/" z)) is Element of the carrier of L
[x,(y "\/" z)] is V33() set
{x,(y "\/" z)} is non empty set
{{x,(y "\/" z)},{x}} is non empty set
the L_meet of L . [x,(y "\/" z)] is set
x "/\" z is Element of the carrier of L
the L_meet of L . (x,z) is Element of the carrier of L
[x,z] is V33() set
{x,z} is non empty set
{{x,z},{x}} is non empty set
the L_meet of L . [x,z] is set
(x "/\" y) "\/" (x "/\" z) is Element of the carrier of L
the L_join of L . ((x "/\" y),(x "/\" z)) is Element of the carrier of L
[(x "/\" y),(x "/\" z)] is V33() set
{(x "/\" y),(x "/\" z)} is non empty set
{(x "/\" y)} is non empty set
{{(x "/\" y),(x "/\" z)},{(x "/\" y)}} is non empty set
the L_join of L . [(x "/\" y),(x "/\" z)] is set
x "/\" z is Element of the carrier of L
x "/\" y is Element of the carrier of L
(x "/\" z) "\/" (x "/\" y) is Element of the carrier of L
the L_join of L . ((x "/\" z),(x "/\" y)) is Element of the carrier of L
[(x "/\" z),(x "/\" y)] is V33() set
{(x "/\" z),(x "/\" y)} is non empty set
{(x "/\" z)} is non empty set
{{(x "/\" z),(x "/\" y)},{(x "/\" z)}} is non empty set
the L_join of L . [(x "/\" z),(x "/\" y)] is set
(x "/\" y) "\/" (x "/\" z) is Element of the carrier of L
the L_join of L . ((x "/\" y),(x "/\" z)) is Element of the carrier of L
[(x "/\" y),(x "/\" z)] is V33() set
{(x "/\" y),(x "/\" z)} is non empty set
{(x "/\" y)} is non empty set
{{(x "/\" y),(x "/\" z)},{(x "/\" y)}} is non empty set
the L_join of L . [(x "/\" y),(x "/\" z)] is set
(L,x,((x "/\" y) "\/" (x "/\" z))) is Element of the carrier of L
y "\/" z is Element of the carrier of L
x "/\" (y "\/" z) is Element of the carrier of L
the L_meet of L . (x,(y "\/" z)) is Element of the carrier of L
[x,(y "\/" z)] is V33() set
{x,(y "\/" z)} is non empty set
{{x,(y "\/" z)},{x}} is non empty set
the L_meet of L . [x,(y "\/" z)] is set
x "/\" (L,x,((x "/\" y) "\/" (x "/\" z))) is Element of the carrier of L
the L_meet of L . (x,(L,x,((x "/\" y) "\/" (x "/\" z)))) is Element of the carrier of L
[x,(L,x,((x "/\" y) "\/" (x "/\" z)))] is V33() set
{x,(L,x,((x "/\" y) "\/" (x "/\" z)))} is non empty set
{{x,(L,x,((x "/\" y) "\/" (x "/\" z)))},{x}} is non empty set
the L_meet of L . [x,(L,x,((x "/\" y) "\/" (x "/\" z)))] 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 LattStr
the carrier of L is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
x ` is Element of the carrier of L
(x `) "\/" y 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 V36([: 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_join of L . ((x `),y) is Element of the carrier of L
[(x `),y] is V33() set
{(x `),y} is non empty set
{(x `)} is non empty set
{{(x `),y},{(x `)}} is non empty set
the L_join of L . [(x `),y] is set
z is Element of the carrier of L
x "/\" z 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 V36([: 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 L_meet of L . (x,z) is Element of the carrier of L
[x,z] is V33() set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
the L_meet of L . [x,z] is set
x "/\" z is Element of the carrier of L
j is Element of the carrier of L
x "/\" j is Element of the carrier of L
the L_meet of L . (x,j) is Element of the carrier of L
[x,j] is V33() set
{x,j} is non empty set
{{x,j},{x}} is non empty set
the L_meet of L . [x,j] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded () LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
(L,x,y) is Element of the carrier of L
z is non empty final meet-closed join-closed Element of bool the carrier of L
x "/\" (L,x,y) 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 V36([: 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 . (x,(L,x,y)) is Element of the carrier of L
[x,(L,x,y)] is V33() set
{x,(L,x,y)} is non empty set
{x} is non empty set
{{x,(L,x,y)},{x}} is non empty set
the L_meet of L . [x,(L,x,y)] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded () LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
(L,y,x) is Element of the carrier of L
z is non empty final meet-closed join-closed Element of bool the carrier of L
x "/\" y 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 V36([: 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 . (x,y) is Element of the carrier of L
[x,y] is V33() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the L_meet of L . [x,y] 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
x is non empty Element of bool the carrier of L
y is non empty Element of bool the carrier of L
{ (b<sub>1</sub> "/\" b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of L : ( b<sub>1</sub> in x & b<sub>2</sub> in y ) } is set
the Element of x is Element of x
the Element of y is Element of y
k is Element of the carrier of L
FI is Element of the carrier of L
k "/\" FI 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 V36([: 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 . (k,FI) is Element of the carrier of L
[k,FI] is V33() set
{k,FI} is non empty set
{k} is non empty set
{{k,FI},{k}} is non empty set
the L_meet of L . [k,FI] is set
a is non empty set
b is set
c is Element of the carrier of L
j is Element of the carrier of L
c "/\" j is Element of the carrier of L
the L_meet of L . (c,j) is Element of the carrier of L
[c,j] is V33() set
{c,j} is non empty set
{c} is non empty set
{{c,j},{c}} is non empty set
the L_meet of L . [c,j] 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
x is non empty Element of bool the carrier of L
y is non empty Element of bool the carrier of L
(L,x,y) is Element of bool the carrier of L
{ (b<sub>1</sub> "/\" b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of L : ( b<sub>1</sub> in x & b<sub>2</sub> in y ) } is set
the Element of x is Element of x
the Element of y is Element of y
k is Element of the carrier of L
FI is Element of the carrier of L
k "/\" FI 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 V36([: 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 . (k,FI) is Element of the carrier of L
[k,FI] is V33() set
{k,FI} is non empty set
{k} is non empty set
{{k,FI},{k}} is non empty set
the L_meet of L . [k,FI] 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
x is Element of the carrier of L
z is non empty Element of bool the carrier of L
y is Element of the carrier of L
j is non empty Element of bool the carrier of L
x "/\" y 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 V36([: 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 . (x,y) is Element of the carrier of L
[x,y] is V33() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the L_meet of L . [x,y] is set
(L,z,j) is non empty Element of bool the carrier of L
{ (b<sub>1</sub> "/\" b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of L : ( b<sub>1</sub> in z & b<sub>2</sub> in j ) } is set
y "/\" x is Element of the carrier of L
the L_meet of L . (y,x) is Element of the carrier of L
[y,x] is V33() set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
the L_meet of L . [y,x] 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
x is set
y is non empty Element of bool the carrier of L
z is non empty Element of bool the carrier of L
(L,y,z) is non empty Element of bool the carrier of L
{ (b<sub>1</sub> "/\" b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of L : ( b<sub>1</sub> in y & b<sub>2</sub> in z ) } 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
x is non empty Element of bool the carrier of L
y is non empty Element of bool the carrier of L
(L,x,y) is non empty Element of bool the carrier of L
{ (b<sub>1</sub> "/\" b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of L : ( b<sub>1</sub> in x & b<sub>2</sub> in y ) } is set
(L,y,x) is non empty Element of bool the carrier of L
{ (b<sub>1</sub> "/\" b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of L : ( b<sub>1</sub> in y & b<sub>2</sub> in x ) } is set
z is non empty Element of bool the carrier of L
j is non empty Element of bool the carrier of L
(L,z,j) is non empty Element of bool the carrier of L
{ (b<sub>1</sub> "/\" b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of L : ( b<sub>1</sub> in z & b<sub>2</sub> in j ) } is set
(L,j,z) is non empty Element of bool the carrier of L
{ (b<sub>1</sub> "/\" b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of L : ( b<sub>1</sub> in j & b<sub>2</sub> in z ) } is set
k is set
FI is Element of the carrier of L
a is Element of the carrier of L
FI "/\" a 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 V36([: 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 . (FI,a) is Element of the carrier of L
[FI,a] is V33() set
{FI,a} is non empty set
{FI} is non empty set
{{FI,a},{FI}} is non empty set
the L_meet of L . [FI,a] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
x is non empty final meet-closed join-closed Element of bool the carrier of L
y is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x,y) is non empty Element of bool the carrier of L
{ (b<sub>1</sub> "/\" b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of L : ( b<sub>1</sub> in x & b<sub>2</sub> in y ) } is set
z is Element of the carrier of L
j is Element of the carrier of L
z "/\" j 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 V36([: 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 . (z,j) is Element of the carrier of L
[z,j] is V33() set
{z,j} is non empty set
{z} is non empty set
{{z,j},{z}} is non empty set
the L_meet of L . [z,j] is set
z "\/" (z "/\" j) 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 V36([: 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 L_join of L . (z,(z "/\" j)) is Element of the carrier of L
[z,(z "/\" j)] is V33() set
{z,(z "/\" j)} is non empty set
{{z,(z "/\" j)},{z}} is non empty set
the L_join of L . [z,(z "/\" j)] is set
j "\/" (z "/\" j) is Element of the carrier of L
the L_join of L . (j,(z "/\" j)) is Element of the carrier of L
[j,(z "/\" j)] is V33() set
{j,(z "/\" j)} is non empty set
{j} is non empty set
{{j,(z "/\" j)},{j}} is non empty set
the L_join of L . [j,(z "/\" j)] is set
k is Element of the carrier of L
FI is Element of the carrier of L
k "/\" FI is Element of the carrier of L
the L_meet of L . (k,FI) is Element of the carrier of L
[k,FI] is V33() set
{k,FI} is non empty set
{k} is non empty set
{{k,FI},{k}} is non empty set
the L_meet of L . [k,FI] is set
a is Element of the carrier of L
b is Element of the carrier of L
a "/\" b is Element of the carrier of L
the L_meet of L . (a,b) is Element of the carrier of L
[a,b] is V33() set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
the L_meet of L . [a,b] is set
(k "/\" FI) "/\" a is Element of the carrier of L
the L_meet of L . ((k "/\" FI),a) is Element of the carrier of L
[(k "/\" FI),a] is V33() set
{(k "/\" FI),a} is non empty set
{(k "/\" FI)} is non empty set
{{(k "/\" FI),a},{(k "/\" FI)}} is non empty set
the L_meet of L . [(k "/\" FI),a] is set
((k "/\" FI) "/\" a) "/\" b is Element of the carrier of L
the L_meet of L . (((k "/\" FI) "/\" a),b) is Element of the carrier of L
[((k "/\" FI) "/\" a),b] is V33() set
{((k "/\" FI) "/\" a),b} is non empty set
{((k "/\" FI) "/\" a)} is non empty set
{{((k "/\" FI) "/\" a),b},{((k "/\" FI) "/\" a)}} is non empty set
the L_meet of L . [((k "/\" FI) "/\" a),b] is set
k "/\" a is Element of the carrier of L
the L_meet of L . (k,a) is Element of the carrier of L
[k,a] is V33() set
{k,a} is non empty set
{{k,a},{k}} is non empty set
the L_meet of L . [k,a] is set
(k "/\" a) "/\" FI is Element of the carrier of L
the L_meet of L . ((k "/\" a),FI) is Element of the carrier of L
[(k "/\" a),FI] is V33() set
{(k "/\" a),FI} is non empty set
{(k "/\" a)} is non empty set
{{(k "/\" a),FI},{(k "/\" a)}} is non empty set
the L_meet of L . [(k "/\" a),FI] is set
((k "/\" a) "/\" FI) "/\" b is Element of the carrier of L
the L_meet of L . (((k "/\" a) "/\" FI),b) is Element of the carrier of L
[((k "/\" a) "/\" FI),b] is V33() set
{((k "/\" a) "/\" FI),b} is non empty set
{((k "/\" a) "/\" FI)} is non empty set
{{((k "/\" a) "/\" FI),b},{((k "/\" a) "/\" FI)}} is non empty set
the L_meet of L . [((k "/\" a) "/\" FI),b] is set
FI "/\" b is Element of the carrier of L
the L_meet of L . (FI,b) is Element of the carrier of L
[FI,b] is V33() set
{FI,b} is non empty set
{FI} is non empty set
{{FI,b},{FI}} is non empty set
the L_meet of L . [FI,b] is set
(k "/\" a) "/\" (FI "/\" b) is Element of the carrier of L
the L_meet of L . ((k "/\" a),(FI "/\" b)) is Element of the carrier of L
[(k "/\" a),(FI "/\" b)] is V33() set
{(k "/\" a),(FI "/\" b)} is non empty set
{{(k "/\" a),(FI "/\" b)},{(k "/\" a)}} is non empty set
the L_meet of L . [(k "/\" a),(FI "/\" b)] is set
k is Element of the carrier of L
FI is Element of the carrier of L
k "/\" FI is Element of the carrier of L
the L_meet of L . (k,FI) is Element of the carrier of L
[k,FI] is V33() set
{k,FI} is non empty set
{k} is non empty set
{{k,FI},{k}} is non empty set
the L_meet of L . [k,FI] is set
j "\/" k is Element of the carrier of L
the L_join of L . (j,k) is Element of the carrier of L
[j,k] is V33() set
{j,k} is non empty set
{{j,k},{j}} is non empty set
the L_join of L . [j,k] is set
j "\/" FI is Element of the carrier of L
the L_join of L . (j,FI) is Element of the carrier of L
[j,FI] is V33() set
{j,FI} is non empty set
{{j,FI},{j}} is non empty set
the L_join of L . [j,FI] is set
z "\/" (k "/\" FI) is Element of the carrier of L
the L_join of L . (z,(k "/\" FI)) is Element of the carrier of L
[z,(k "/\" FI)] is V33() set
{z,(k "/\" FI)} is non empty set
{{z,(k "/\" FI)},{z}} is non empty set
the L_join of L . [z,(k "/\" FI)] is set
z "\/" k is Element of the carrier of L
the L_join of L . (z,k) is Element of the carrier of L
[z,k] is V33() set
{z,k} is non empty set
{{z,k},{z}} is non empty set
the L_join of L . [z,k] is set
z "\/" FI is Element of the carrier of L
the L_join of L . (z,FI) is Element of the carrier of L
[z,FI] is V33() set
{z,FI} is non empty set
{{z,FI},{z}} is non empty set
the L_join of L . [z,FI] is set
(z "\/" k) "/\" (z "\/" FI) is Element of the carrier of L
the L_meet of L . ((z "\/" k),(z "\/" FI)) is Element of the carrier of L
[(z "\/" k),(z "\/" FI)] is V33() set
{(z "\/" k),(z "\/" FI)} is non empty set
{(z "\/" k)} is non empty set
{{(z "\/" k),(z "\/" FI)},{(z "\/" k)}} is non empty set
the L_meet of L . [(z "\/" k),(z "\/" FI)] is set
j "\/" (k "/\" FI) is Element of the carrier of L
the L_join of L . (j,(k "/\" FI)) is Element of the carrier of L
[j,(k "/\" FI)] is V33() set
{j,(k "/\" FI)} is non empty set
{{j,(k "/\" FI)},{j}} is non empty set
the L_join of L . [j,(k "/\" FI)] is set
(j "\/" k) "/\" (j "\/" FI) is Element of the carrier of L
the L_meet of L . ((j "\/" k),(j "\/" FI)) is Element of the carrier of L
[(j "\/" k),(j "\/" FI)] is V33() set
{(j "\/" k),(j "\/" FI)} is non empty set
{(j "\/" k)} is non empty set
{{(j "\/" k),(j "\/" FI)},{(j "\/" k)}} is non empty set
the L_meet of L . [(j "\/" k),(j "\/" FI)] 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
x is non empty Element of bool the carrier of L
(L,x) is non empty final meet-closed join-closed Element of bool the carrier of L
y is non empty Element of bool the carrier of L
x \/ y is non empty Element of bool the carrier of L
(L,(x \/ y)) is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x) \/ y is non empty Element of bool the carrier of L
(L,((L,x) \/ y)) is non empty final meet-closed join-closed Element of bool the carrier of L
(L,y) is non empty final meet-closed join-closed Element of bool the carrier of L
x \/ (L,y) is non empty Element of bool the carrier of L
(L,(x \/ (L,y))) is non empty final meet-closed join-closed Element of bool the carrier of L
j is non empty Element of bool the carrier of L
z is non empty Element of bool the carrier of L
z \/ j is non empty Element of bool the carrier of L
(L,(z \/ j)) is non empty final meet-closed join-closed Element of bool the carrier of L
(L,z) is non empty final meet-closed join-closed Element of bool the carrier of L
(L,z) \/ j is non empty Element of bool the carrier of L
(L,((L,z) \/ j)) 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
bool the carrier of L is non empty set
x is non empty final meet-closed join-closed Element of bool the carrier of L
y is non empty final meet-closed join-closed Element of bool the carrier of L
x \/ y is non empty Element of bool the carrier of L
(L,(x \/ y)) is non empty final meet-closed join-closed Element of bool the carrier of L
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of L : ex b<sub>2</sub>, b<sub>3</sub> being Element of the carrier of L st
( b<sub>2</sub> "/\" b<sub>3</sub> [= b<sub>1</sub> & b<sub>2</sub> in x & b<sub>3</sub> in y ) } is set
j is Element of the carrier of L
k is Element of the carrier of L
j "/\" 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 V36([: 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 . (j,k) is Element of the carrier of L
[j,k] is V33() set
{j,k} is non empty set
{j} is non empty set
{{j,k},{j}} is non empty set
the L_meet of L . [j,k] is set
FI is non empty set
a is set
b is Element of the carrier of L
c is Element of the carrier of L
j is Element of the carrier of L
c "/\" j is Element of the carrier of L
the L_meet of L . (c,j) is Element of the carrier of L
[c,j] is V33() set
{c,j} is non empty set
{c} is non empty set
{{c,j},{c}} is non empty set
the L_meet of L . [c,j] is set
a is non empty Element of bool the carrier of L
b is Element of the carrier of L
c is Element of the carrier of L
j is Element of the carrier of L
r9 is Element of the carrier of L
s9 is Element of the carrier of L
r9 "/\" s9 is Element of the carrier of L
the L_meet of L . (r9,s9) is Element of the carrier of L
[r9,s9] is V33() set
{r9,s9} is non empty set
{r9} is non empty set
{{r9,s9},{r9}} is non empty set
the L_meet of L . [r9,s9] is set
j is Element of the carrier of L
r9 is Element of the carrier of L
j "/\" r9 is Element of the carrier of L
the L_meet of L . (j,r9) is Element of the carrier of L
[j,r9] is V33() set
{j,r9} is non empty set
{j} is non empty set
{{j,r9},{j}} is non empty set
the L_meet of L . [j,r9] is set
b is Element of the carrier of L
c is Element of the carrier of L
b "/\" c is Element of the carrier of L
the L_meet of L . (b,c) is Element of the carrier of L
[b,c] is V33() set
{b,c} is non empty set
{b} is non empty set
{{b,c},{b}} is non empty set
the L_meet of L . [b,c] is set
j is Element of the carrier of L
r9 is Element of the carrier of L
s9 is Element of the carrier of L
r9 "/\" s9 is Element of the carrier of L
the L_meet of L . (r9,s9) is Element of the carrier of L
[r9,s9] is V33() set
{r9,s9} is non empty set
{r9} is non empty set
{{r9,s9},{r9}} is non empty set
the L_meet of L . [r9,s9] is set
j is Element of the carrier of L
r9 is Element of the carrier of L
j "/\" r9 is Element of the carrier of L
the L_meet of L . (j,r9) is Element of the carrier of L
[j,r9] is V33() set
{j,r9} is non empty set
{j} is non empty set
{{j,r9},{j}} is non empty set
the L_meet of L . [j,r9] is set
s9 is Element of the carrier of L
s is Element of the carrier of L
r1 is Element of the carrier of L
s "/\" r1 is Element of the carrier of L
the L_meet of L . (s,r1) is Element of the carrier of L
[s,r1] is V33() set
{s,r1} is non empty set
{s} is non empty set
{{s,r1},{s}} is non empty set
the L_meet of L . [s,r1] is set
s9 is Element of the carrier of L
s is Element of the carrier of L
s9 "/\" s is Element of the carrier of L
the L_meet of L . (s9,s) is Element of the carrier of L
[s9,s] is V33() set
{s9,s} is non empty set
{s9} is non empty set
{{s9,s},{s9}} is non empty set
the L_meet of L . [s9,s] is set
b "/\" (s9 "/\" s) is Element of the carrier of L
the L_meet of L . (b,(s9 "/\" s)) is Element of the carrier of L
[b,(s9 "/\" s)] is V33() set
{b,(s9 "/\" s)} is non empty set
{{b,(s9 "/\" s)},{b}} is non empty set
the L_meet of L . [b,(s9 "/\" s)] is set
(j "/\" r9) "/\" (s9 "/\" s) is Element of the carrier of L
the L_meet of L . ((j "/\" r9),(s9 "/\" s)) is Element of the carrier of L
[(j "/\" r9),(s9 "/\" s)] is V33() set
{(j "/\" r9),(s9 "/\" s)} is non empty set
{(j "/\" r9)} is non empty set
{{(j "/\" r9),(s9 "/\" s)},{(j "/\" r9)}} is non empty set
the L_meet of L . [(j "/\" r9),(s9 "/\" s)] is set
(j "/\" r9) "/\" s9 is Element of the carrier of L
the L_meet of L . ((j "/\" r9),s9) is Element of the carrier of L
[(j "/\" r9),s9] is V33() set
{(j "/\" r9),s9} is non empty set
{{(j "/\" r9),s9},{(j "/\" r9)}} is non empty set
the L_meet of L . [(j "/\" r9),s9] is set
((j "/\" r9) "/\" s9) "/\" s is Element of the carrier of L
the L_meet of L . (((j "/\" r9) "/\" s9),s) is Element of the carrier of L
[((j "/\" r9) "/\" s9),s] is V33() set
{((j "/\" r9) "/\" s9),s} is non empty set
{((j "/\" r9) "/\" s9)} is non empty set
{{((j "/\" r9) "/\" s9),s},{((j "/\" r9) "/\" s9)}} is non empty set
the L_meet of L . [((j "/\" r9) "/\" s9),s] is set
j "/\" s9 is Element of the carrier of L
the L_meet of L . (j,s9) is Element of the carrier of L
[j,s9] is V33() set
{j,s9} is non empty set
{{j,s9},{j}} is non empty set
the L_meet of L . [j,s9] is set
(j "/\" s9) "/\" r9 is Element of the carrier of L
the L_meet of L . ((j "/\" s9),r9) is Element of the carrier of L
[(j "/\" s9),r9] is V33() set
{(j "/\" s9),r9} is non empty set
{(j "/\" s9)} is non empty set
{{(j "/\" s9),r9},{(j "/\" s9)}} is non empty set
the L_meet of L . [(j "/\" s9),r9] is set
((j "/\" s9) "/\" r9) "/\" s is Element of the carrier of L
the L_meet of L . (((j "/\" s9) "/\" r9),s) is Element of the carrier of L
[((j "/\" s9) "/\" r9),s] is V33() set
{((j "/\" s9) "/\" r9),s} is non empty set
{((j "/\" s9) "/\" r9)} is non empty set
{{((j "/\" s9) "/\" r9),s},{((j "/\" s9) "/\" r9)}} is non empty set
the L_meet of L . [((j "/\" s9) "/\" r9),s] is set
r9 "/\" s is Element of the carrier of L
the L_meet of L . (r9,s) is Element of the carrier of L
[r9,s] is V33() set
{r9,s} is non empty set
{r9} is non empty set
{{r9,s},{r9}} is non empty set
the L_meet of L . [r9,s] is set
(j "/\" s9) "/\" (r9 "/\" s) is Element of the carrier of L
the L_meet of L . ((j "/\" s9),(r9 "/\" s)) is Element of the carrier of L
[(j "/\" s9),(r9 "/\" s)] is V33() set
{(j "/\" s9),(r9 "/\" s)} is non empty set
{{(j "/\" s9),(r9 "/\" s)},{(j "/\" s9)}} is non empty set
the L_meet of L . [(j "/\" s9),(r9 "/\" s)] is set
b is non empty final meet-closed join-closed Element of bool the carrier of L
c is set
j is Element of y
j "/\" j is Element of the carrier of L
the L_meet of L . (j,j) is Element of the carrier of L
[j,j] is V33() set
{j,j} is non empty set
{j} is non empty set
{{j,j},{j}} is non empty set
the L_meet of L . [j,j] is set
c is set
j is Element of x
j "/\" k is Element of the carrier of L
the L_meet of L . (j,k) is Element of the carrier of L
[j,k] is V33() set
{j,k} is non empty set
{j} is non empty set
{{j,k},{j}} is non empty set
the L_meet of L . [j,k] is set
c is set
j is Element of the carrier of L
r9 is Element of the carrier of L
s9 is Element of the carrier of L
r9 "/\" s9 is Element of the carrier of L
the L_meet of L . (r9,s9) is Element of the carrier of L
[r9,s9] is V33() set
{r9,s9} is non empty set
{r9} is non empty set
{{r9,s9},{r9}} is non empty set
the L_meet of L . [r9,s9] is set
r9 is Element of the carrier of L
s9 is Element of the carrier of L
r9 "/\" s9 is Element of the carrier of L
the L_meet of L . (r9,s9) is Element of the carrier of L
[r9,s9] is V33() set
{r9,s9} is non empty set
{r9} is non empty set
{{r9,s9},{r9}} is non empty set
the L_meet of L . [r9,s9] 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
x is non empty final meet-closed join-closed Element of bool the carrier of L
y is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x,y) is non empty Element of bool the carrier of L
{ (b<sub>1</sub> "/\" b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of L : ( b<sub>1</sub> in x & b<sub>2</sub> in y ) } is set
z is non empty final meet-closed join-closed Element of bool the carrier of L
j is non empty final meet-closed join-closed Element of bool the carrier of L
(L,z,j) is non empty Element of bool the carrier of L
{ (b<sub>1</sub> "/\" b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of L : ( b<sub>1</sub> in z & b<sub>2</sub> in j ) } is set
k is set
a is Element of the carrier of L
FI is Element of the carrier of L
FI "\/" a 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 V36([: 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_join of L . (FI,a) is Element of the carrier of L
[FI,a] is V33() set
{FI,a} is non empty set
{FI} is non empty set
{{FI,a},{FI}} is non empty set
the L_join of L . [FI,a] is set
FI "/\" (FI "\/" a) 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 V36([: 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 L_meet of L . (FI,(FI "\/" a)) is Element of the carrier of L
[FI,(FI "\/" a)] is V33() set
{FI,(FI "\/" a)} is non empty set
{{FI,(FI "\/" a)},{FI}} is non empty set
the L_meet of L . [FI,(FI "\/" a)] is set
a "\/" FI is Element of the carrier of L
the L_join of L . (a,FI) is Element of the carrier of L
[a,FI] is V33() set
{a,FI} is non empty set
{a} is non empty set
{{a,FI},{a}} is non empty set
the L_join of L . [a,FI] is set
(L,y,x) is non empty Element of bool the carrier of L
{ (b<sub>1</sub> "/\" b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of L : ( b<sub>1</sub> in y & b<sub>2</sub> in x ) } 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
x is non empty final meet-closed join-closed Element of bool the carrier of L
y is non empty final meet-closed join-closed Element of bool the carrier of L
x \/ y is non empty Element of bool the carrier of L
(L,(x \/ y)) is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x,y) is non empty Element of bool the carrier of L
{ (b<sub>1</sub> "/\" b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of L : ( b<sub>1</sub> in x & b<sub>2</sub> in y ) } is set
(L,(L,x,y)) is non empty final meet-closed join-closed Element of bool the carrier of L
z is set
j is Element of the carrier of L
k is Element of the carrier of L
j "/\" 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 V36([: 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 . (j,k) is Element of the carrier of L
[j,k] is V33() set
{j,k} is non empty set
{j} is non empty set
{{j,k},{j}} is non empty set
the L_meet of L . [j,k] is set
(L,(L,(x \/ y))) 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 distributive modular upper-bounded () LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
x is non empty final meet-closed join-closed Element of bool the carrier of L
y is non empty final meet-closed join-closed Element of bool the carrier of L
x \/ y is non empty Element of bool the carrier of L
(L,(x \/ y)) is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x,y) is non empty final meet-closed join-closed Element of bool the carrier of L
{ (b<sub>1</sub> "/\" b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of L : ( b<sub>1</sub> in x & b<sub>2</sub> in y ) } is set
(L,(L,x,y)) 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 distributive modular lower-bounded upper-bounded bounded complemented Boolean () LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
x is non empty final meet-closed join-closed Element of bool the carrier of L
y is non empty final meet-closed join-closed Element of bool the carrier of L
x \/ y is non empty Element of bool the carrier of L
(L,(x \/ y)) is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x,y) is non empty final meet-closed join-closed Element of bool the carrier of L
{ (b<sub>1</sub> "/\" b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of L : ( b<sub>1</sub> in x & b<sub>2</sub> in y ) } is set
(L,(L,x,y)) 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 distributive modular upper-bounded () LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
{y} is non empty Element of bool the carrier of L
(L,y,x) is Element of the carrier of L
z is non empty Element of bool the carrier of L
z \/ {y} is non empty Element of bool the carrier of L
(L,(z \/ {y})) is non empty final meet-closed join-closed Element of bool the carrier of L
(L,z) is non empty final meet-closed join-closed Element of bool the carrier of L
(L,z) \/ {y} is non empty Element of bool the carrier of L
(L,((L,z) \/ {y})) is non empty final meet-closed join-closed Element of bool the carrier of L
(L,{y}) is non empty final meet-closed join-closed Element of bool the carrier of L
(L,z) \/ (L,{y}) is non empty Element of bool the carrier of L
(L,((L,z) \/ (L,{y}))) is non empty final meet-closed join-closed Element of bool the carrier of L
(L,y) is non empty final meet-closed join-closed Element of bool the carrier of L
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of L : y [= b<sub>1</sub> } is set
(L,z) \/ (L,y) is non empty Element of bool the carrier of L
(L,((L,z) \/ (L,y))) is non empty final meet-closed join-closed Element of bool the carrier of L
(L,(L,z),(L,y)) is non empty final meet-closed join-closed Element of bool the carrier of L
{ (b<sub>1</sub> "/\" b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of L : ( b<sub>1</sub> in (L,z) & b<sub>2</sub> in (L,y) ) } is set
j is Element of the carrier of L
k is Element of the carrier of L
j "/\" 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 V36([: 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 . (j,k) is Element of the carrier of L
[j,k] is V33() set
{j,k} is non empty set
{j} is non empty set
{{j,k},{j}} is non empty set
the L_meet of L . [j,k] is set
j "/\" y is Element of the carrier of L
the L_meet of L . (j,y) is Element of the carrier of L
[j,y] is V33() set
{j,y} is non empty set
{{j,y},{j}} is non empty set
the L_meet of L . [j,y] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded () LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
(L,x,y) is Element of the carrier of L
z is Element of the carrier of L
(L,y,z) is Element of the carrier of L
(L,x,z) is Element of the carrier of L
j is non empty final meet-closed join-closed Element of bool the carrier of L
{x} is non empty Element of bool the carrier of L
j \/ {x} is non empty Element of bool the carrier of L
(L,(j \/ {x})) is non empty final meet-closed join-closed Element of bool the carrier of L
(L,j) 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 distributive modular lower-bounded upper-bounded bounded complemented Boolean () LattStr
the carrier of L is non empty set
x is Element of the carrier of L
x ` is Element of the carrier of L
y is Element of the carrier of L
(L,x,y) is Element of the carrier of L
(x `) "\/" y 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 V36([: 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_join of L . ((x `),y) is Element of the carrier of L
[(x `),y] is V33() set
{(x `),y} is non empty set
{(x `)} is non empty set
{{(x `),y},{(x `)}} is non empty set
the L_join of L . [(x `),y] is set
x "/\" ((x `) "\/" y) 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 V36([: 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 L_meet of L . (x,((x `) "\/" y)) is Element of the carrier of L
[x,((x `) "\/" y)] is V33() set
{x,((x `) "\/" y)} is non empty set
{x} is non empty set
{{x,((x `) "\/" y)},{x}} is non empty set
the L_meet of L . [x,((x `) "\/" y)] is set
z is Element of the carrier of L
x "/\" z is Element of the carrier of L
the L_meet of L . (x,z) is Element of the carrier of L
[x,z] is V33() set
{x,z} is non empty set
{{x,z},{x}} is non empty set
the L_meet of L . [x,z] 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 () LattStr
the carrier of L is non empty set
Bottom L is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
y ` is Element of the carrier of L
x "/\" (y `) 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 V36([: 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 . (x,(y `)) is Element of the carrier of L
[x,(y `)] is V33() set
{x,(y `)} is non empty set
{x} is non empty set
{{x,(y `)},{x}} is non empty set
the L_meet of L . [x,(y `)] is set
z is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of z is non empty set
j is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of j is non empty set
k is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of k is non empty set
x "/\" y is Element of the carrier of L
the L_meet of L . (x,y) is Element of the carrier of L
[x,y] is V33() set
{x,y} is non empty set
{{x,y},{x}} is non empty set
the L_meet of L . [x,y] is set
y "/\" (y `) is Element of the carrier of L
the L_meet of L . (y,(y `)) is Element of the carrier of L
[y,(y `)] is V33() set
{y,(y `)} is non empty set
{y} is non empty set
{{y,(y `)},{y}} is non empty set
the L_meet of L . [y,(y `)] is set
x "/\" (y "/\" (y `)) is Element of the carrier of L
the L_meet of L . (x,(y "/\" (y `))) is Element of the carrier of L
[x,(y "/\" (y `))] is V33() set
{x,(y "/\" (y `))} is non empty set
{{x,(y "/\" (y `))},{x}} is non empty set
the L_meet of L . [x,(y "/\" (y `))] is set
FI is Element of the carrier of z
Bottom z is Element of the carrier of z
FI "/\" (Bottom z) is Element of the carrier of z
the L_meet of z is Relation-like [: the carrier of z, the carrier of z:] -defined the carrier of z -valued Function-like V36([: the carrier of z, the carrier of z:], the carrier of z) Element of bool [:[: the carrier of z, the carrier of z:], the carrier of z:]
[: the carrier of z, the carrier of z:] is non empty set
[:[: the carrier of z, the carrier of z:], the carrier of z:] is non empty set
bool [:[: the carrier of z, the carrier of z:], the carrier of z:] is non empty set
the L_meet of z . (FI,(Bottom z)) is Element of the carrier of z
[FI,(Bottom z)] is V33() set
{FI,(Bottom z)} is non empty set
{FI} is non empty set
{{FI,(Bottom z)},{FI}} is non empty set
the L_meet of z . [FI,(Bottom z)] is set
a is Element of the carrier of z
b is Element of the carrier of z
a "\/" b is Element of the carrier of z
the L_join of z is Relation-like [: the carrier of z, the carrier of z:] -defined the carrier of z -valued Function-like V36([: the carrier of z, the carrier of z:], the carrier of z) Element of bool [:[: the carrier of z, the carrier of z:], the carrier of z:]
[: the carrier of z, the carrier of z:] is non empty set
[:[: the carrier of z, the carrier of z:], the carrier of z:] is non empty set
bool [:[: the carrier of z, the carrier of z:], the carrier of z:] is non empty set
the L_join of z . (a,b) is Element of the carrier of z
[a,b] is V33() set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
the L_join of z . [a,b] is set
s9 is Element of the carrier of k
r9 is Element of the carrier of k
s9 "\/" r9 is Element of the carrier of k
the L_join of k is Relation-like [: the carrier of k, the carrier of k:] -defined the carrier of k -valued Function-like V36([: the carrier of k, the carrier of k:], the carrier of k) Element of bool [:[: the carrier of k, the carrier of k:], the carrier of k:]
[: the carrier of k, the carrier of k:] is non empty set
[:[: the carrier of k, the carrier of k:], the carrier of k:] is non empty set
bool [:[: the carrier of k, the carrier of k:], the carrier of k:] is non empty set
the L_join of k . (s9,r9) is Element of the carrier of k
[s9,r9] is V33() set
{s9,r9} is non empty set
{s9} is non empty set
{{s9,r9},{s9}} is non empty set
the L_join of k . [s9,r9] is set
s9 ` is Element of the carrier of k
s9 "\/" (s9 `) is Element of the carrier of k
the L_join of k . (s9,(s9 `)) is Element of the carrier of k
[s9,(s9 `)] is V33() set
{s9,(s9 `)} is non empty set
{{s9,(s9 `)},{s9}} is non empty set
the L_join of k . [s9,(s9 `)] is set
(s9 "\/" r9) "/\" (s9 "\/" (s9 `)) is Element of the carrier of k
the L_meet of k is Relation-like [: the carrier of k, the carrier of k:] -defined the carrier of k -valued Function-like V36([: the carrier of k, the carrier of k:], the carrier of k) Element of bool [:[: the carrier of k, the carrier of k:], the carrier of k:]
the L_meet of k . ((s9 "\/" r9),(s9 "\/" (s9 `))) is Element of the carrier of k
[(s9 "\/" r9),(s9 "\/" (s9 `))] is V33() set
{(s9 "\/" r9),(s9 "\/" (s9 `))} is non empty set
{(s9 "\/" r9)} is non empty set
{{(s9 "\/" r9),(s9 "\/" (s9 `))},{(s9 "\/" r9)}} is non empty set
the L_meet of k . [(s9 "\/" r9),(s9 "\/" (s9 `))] is set
j is Element of the carrier of j
c is Element of the carrier of j
j "\/" c is Element of the carrier of j
the L_join of j is Relation-like [: the carrier of j, the carrier of j:] -defined the carrier of j -valued Function-like V36([: the carrier of j, the carrier of j:], the carrier of j) Element of bool [:[: the carrier of j, the carrier of j:], the carrier of j:]
[: the carrier of j, the carrier of j:] is non empty set
[:[: the carrier of j, the carrier of j:], the carrier of j:] is non empty set
bool [:[: the carrier of j, the carrier of j:], the carrier of j:] is non empty set
the L_join of j . (j,c) is Element of the carrier of j
[j,c] is V33() set
{j,c} is non empty set
{j} is non empty set
{{j,c},{j}} is non empty set
the L_join of j . [j,c] is set
Top j is Element of the carrier of j
(j "\/" c) "/\" (Top j) is Element of the carrier of j
the L_meet of j is Relation-like [: the carrier of j, the carrier of j:] -defined the carrier of j -valued Function-like V36([: the carrier of j, the carrier of j:], the carrier of j) Element of bool [:[: the carrier of j, the carrier of j:], the carrier of j:]
the L_meet of j . ((j "\/" c),(Top j)) is Element of the carrier of j
[(j "\/" c),(Top j)] is V33() set
{(j "\/" c),(Top j)} is non empty set
{(j "\/" c)} is non empty set
{{(j "\/" c),(Top j)},{(j "\/" c)}} is non empty set
the L_meet of j . [(j "\/" c),(Top j)] is set
x "\/" y 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 V36([: 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 L_join of L . (x,y) is Element of the carrier of L
[x,y] is V33() set
{x,y} is non empty set
{{x,y},{x}} is non empty set
the L_join of L . [x,y] 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 () LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
x is non empty final meet-closed join-closed Element of bool the carrier of L
z is Element of the carrier of L
z ` is Element of the carrier of L
(L,z) is non empty final meet-closed join-closed Element of bool the carrier of L
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of L : z [= b<sub>1</sub> } is set
x \/ (L,z) is non empty Element of bool the carrier of L
(L,(x \/ (L,z))) is non empty final meet-closed join-closed Element of bool the carrier of L
y is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded () LattStr
the carrier of y is non empty set
bool the carrier of y is non empty set
(L,z,(z `)) is Element of the carrier of L
(z `) "\/" (z `) 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 V36([: 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_join of L . ((z `),(z `)) is Element of the carrier of L
[(z `),(z `)] is V33() set
{(z `),(z `)} is non empty set
{(z `)} is non empty set
{{(z `),(z `)},{(z `)}} is non empty set
the L_join of L . [(z `),(z `)] is set
{z} is non empty Element of bool the carrier of L
(L,{z}) is non empty final meet-closed join-closed Element of bool the carrier of L
j is Element of the carrier of y
j ` is Element of the carrier of y
k is non empty final meet-closed join-closed Element of bool the carrier of y
{j} is non empty Element of bool the carrier of y
k \/ {j} is non empty Element of bool the carrier of y
(y,(k \/ {j})) is non empty final meet-closed join-closed Element of bool the carrier of y
(L,x) is non empty final meet-closed join-closed Element of bool the carrier of L
y is non empty final meet-closed join-closed Element of bool the carrier of L
z is set
j is set
z is set
j is Element of y
j ` is Element of the carrier of L
(j `) "/\" j 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 V36([: 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 . ((j `),j) is Element of the carrier of L
[(j `),j] is V33() set
{(j `),j} is non empty set
{(j `)} is non empty set
{{(j `),j},{(j `)}} is non empty set
the L_meet of L . [(j `),j] is set
Bottom L is Element of the carrier of L
(L,y) 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 distributive modular lower-bounded upper-bounded bounded complemented Boolean () LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
(L) is non empty final meet-closed join-closed Element of bool the carrier of L
x is non empty final meet-closed join-closed Element of bool the carrier of L
y is Element of the carrier of L
y ` is Element of the carrier of L
y "\/" (y `) 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 V36([: 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_join of L . (y,(y `)) is Element of the carrier of L
[y,(y `)] is V33() set
{y,(y `)} is non empty set
{y} is non empty set
{{y,(y `)},{y}} is non empty set
the L_join of L . [y,(y `)] is set
Top L is Element of the carrier of L
y is Element of the carrier of L
z is Element of the carrier of L
y "\/" z 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 V36([: 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_join of L . (y,z) is Element of the carrier of L
[y,z] is V33() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the L_join of L . [y,z] is set
y ` is Element of the carrier of L
z ` is Element of the carrier of L
(y `) "/\" (z `) 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 V36([: 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 L_meet of L . ((y `),(z `)) is Element of the carrier of L
[(y `),(z `)] is V33() set
{(y `),(z `)} is non empty set
{(y `)} is non empty set
{{(y `),(z `)},{(y `)}} is non empty set
the L_meet of L . [(y `),(z `)] is set
(y "\/" z) ` is Element of the carrier of L
(y "\/" z) "/\" ((y "\/" z) `) is Element of the carrier of L
the L_meet of L . ((y "\/" z),((y "\/" z) `)) is Element of the carrier of L
[(y "\/" z),((y "\/" z) `)] is V33() set
{(y "\/" z),((y "\/" z) `)} is non empty set
{(y "\/" z)} is non empty set
{{(y "\/" z),((y "\/" z) `)},{(y "\/" z)}} is non empty set
the L_meet of L . [(y "\/" z),((y "\/" z) `)] is set
Bottom L is Element of the carrier of L
(L,x) 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 distributive modular lower-bounded upper-bounded bounded complemented Boolean () LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
x is non empty final meet-closed join-closed Element of bool the carrier of L
y is Element of the carrier of L
y ` is Element of the carrier of L
y "/\" (y `) 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 V36([: 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 . (y,(y `)) is Element of the carrier of L
[y,(y `)] is V33() set
{y,(y `)} is non empty set
{y} is non empty set
{{y,(y `)},{y}} is non empty set
the L_meet of L . [y,(y `)] is set
Bottom L is Element of the carrier of L
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean () LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
y ` is Element of the carrier of L
x "/\" (y `) 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 V36([: 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 . (x,(y `)) is Element of the carrier of L
[x,(y `)] is V33() set
{x,(y `)} is non empty set
{x} is non empty set
{{x,(y `)},{x}} is non empty set
the L_meet of L . [x,(y `)] is set
Bottom L is Element of the carrier of L
x ` is Element of the carrier of L
y "/\" (x `) is Element of the carrier of L
the L_meet of L . (y,(x `)) is Element of the carrier of L
[y,(x `)] is V33() set
{y,(x `)} is non empty set
{y} is non empty set
{{y,(x `)},{y}} is non empty set
the L_meet of L . [y,(x `)] is set
z is non empty final meet-closed join-closed Element of bool the carrier of L
j is non empty final meet-closed join-closed Element of bool the carrier of L
z 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
bool the carrier of L is non empty set
x is non empty final meet-closed join-closed Element of bool the carrier of L
[:x,x:] is non empty set
[:[:x,x:],x:] is non empty set
bool [:[:x,x:],x:] 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 V36([: 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_join of L || x is set
the L_join of L | [:x,x:] is Relation-like 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 V36([: 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 L_meet of L || x is set
the L_meet of L | [:x,x:] is Relation-like set
j is Relation-like [:x,x:] -defined x -valued Function-like V36([:x,x:],x) Element of bool [:[:x,x:],x:]
k is Relation-like [:x,x:] -defined x -valued Function-like V36([:x,x:],x) Element of bool [:[:x,x:],x:]
y is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
LattStr(# x,j,k #) is non empty strict LattStr
FI is Relation-like [:x,x:] -defined x -valued Function-like V36([:x,x:],x) Element of bool [:[:x,x:],x:]
a is Relation-like [:x,x:] -defined x -valued Function-like V36([:x,x:],x) Element of bool [:[:x,x:],x:]
z is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
LattStr(# x,FI,a #) is non empty strict LattStr
[:x,x:] is non empty Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
bool [: the carrier of L, the carrier of L:] is non empty set
[:[:x,x:], the carrier of L:] is non empty set
bool [:[:x,x:], the carrier of L:] is non empty set
y is Relation-like [:x,x:] -defined the carrier of L -valued Function-like V36([:x,x:], the carrier of L) Element of bool [:[:x,x:], the carrier of L:]
dom y is Relation-like x -defined x -valued Element of bool [:x,x:]
bool [:x,x:] is non empty set
rng y is Element of bool the carrier of L
j is set
k is set
y . k is set
k `1 is set
k `2 is set
[(k `1),(k `2)] is V33() set
{(k `1),(k `2)} is non empty set
{(k `1)} is non empty set
{{(k `1),(k `2)},{(k `1)}} is non empty set
FI is Element of x
a is Element of x
FI "\/" a is Element of the carrier of L
the L_join of L . (FI,a) is Element of the carrier of L
[FI,a] is V33() set
{FI,a} is non empty set
{FI} is non empty set
{{FI,a},{FI}} is non empty set
the L_join of L . [FI,a] is set
z is Relation-like [:x,x:] -defined the carrier of L -valued Function-like V36([:x,x:], the carrier of L) Element of bool [:[:x,x:], the carrier of L:]
dom z is Relation-like x -defined x -valued Element of bool [:x,x:]
rng z is Element of bool the carrier of L
k is set
FI is set
z . FI is set
FI `1 is set
FI `2 is set
[(FI `1),(FI `2)] is V33() set
{(FI `1),(FI `2)} is non empty set
{(FI `1)} is non empty set
{{(FI `1),(FI `2)},{(FI `1)}} is non empty set
a is Element of x
b is Element of x
a "/\" b is Element of the carrier of L
the L_meet of L . (a,b) is Element of the carrier of L
[a,b] is V33() set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
the L_meet of L . [a,b] is set
j is Relation-like [:x,x:] -defined x -valued Function-like V36([:x,x:],x) Element of bool [:[:x,x:],x:]
k is Relation-like [:x,x:] -defined x -valued Function-like V36([:x,x:],x) Element of bool [:[:x,x:],x:]
LattStr(# x,j,k #) is non empty strict LattStr
FI is non empty LattStr
the carrier of FI is non empty set
the L_join of FI is Relation-like [: the carrier of FI, the carrier of FI:] -defined the carrier of FI -valued Function-like V36([: the carrier of FI, the carrier of FI:], the carrier of FI) Element of bool [:[: the carrier of FI, the carrier of FI:], the carrier of FI:]
[: the carrier of FI, the carrier of FI:] is non empty set
[:[: the carrier of FI, the carrier of FI:], the carrier of FI:] is non empty set
bool [:[: the carrier of FI, the carrier of FI:], the carrier of FI:] is non empty set
the L_meet of FI is Relation-like [: the carrier of FI, the carrier of FI:] -defined the carrier of FI -valued Function-like V36([: the carrier of FI, the carrier of FI:], the carrier of FI) Element of bool [:[: the carrier of FI, the carrier of FI:], the carrier of FI:]
a is Element of the carrier of FI
b is Element of the carrier of FI
the L_join of FI . (a,b) is Element of the carrier of FI
[a,b] is V33() set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
the L_join of FI . [a,b] is set
the L_join of L . (a,b) is set
the L_join of L . [a,b] is set
the L_meet of FI . (a,b) is Element of the carrier of FI
the L_meet of FI . [a,b] is set
the L_meet of L . (a,b) is set
the L_meet of L . [a,b] is set
[a,b] is V33() Element of [: the carrier of FI, the carrier of FI:]
the L_join of FI . [a,b] is Element of the carrier of FI
a is Element of the carrier of FI
b is Element of the carrier of FI
c is Element of the carrier of FI
b "/\" c is Element of the carrier of FI
the L_meet of FI . (b,c) is Element of the carrier of FI
[b,c] is V33() set
{b,c} is non empty set
{b} is non empty set
{{b,c},{b}} is non empty set
the L_meet of FI . [b,c] is set
a "/\" (b "/\" c) is Element of the carrier of FI
the L_meet of FI . (a,(b "/\" c)) is Element of the carrier of FI
[a,(b "/\" c)] is V33() set
{a,(b "/\" c)} is non empty set
{a} is non empty set
{{a,(b "/\" c)},{a}} is non empty set
the L_meet of FI . [a,(b "/\" c)] is set
a "/\" b is Element of the carrier of FI
the L_meet of FI . (a,b) is Element of the carrier of FI
[a,b] is V33() set
{a,b} is non empty set
{{a,b},{a}} is non empty set
the L_meet of FI . [a,b] is set
(a "/\" b) "/\" c is Element of the carrier of FI
the L_meet of FI . ((a "/\" b),c) is Element of the carrier of FI
[(a "/\" b),c] is V33() set
{(a "/\" b),c} is non empty set
{(a "/\" b)} is non empty set
{{(a "/\" b),c},{(a "/\" b)}} is non empty set
the L_meet of FI . [(a "/\" b),c] is set
the L_meet of L . (a,(b "/\" c)) is set
the L_meet of L . [a,(b "/\" c)] is set
j is Element of x
r9 is Element of x
s9 is Element of x
r9 "/\" s9 is Element of the carrier of L
the L_meet of L . (r9,s9) is Element of the carrier of L
[r9,s9] is V33() set
{r9,s9} is non empty set
{r9} is non empty set
{{r9,s9},{r9}} is non empty set
the L_meet of L . [r9,s9] is set
j "/\" (r9 "/\" s9) is Element of the carrier of L
the L_meet of L . (j,(r9 "/\" s9)) is Element of the carrier of L
[j,(r9 "/\" s9)] is V33() set
{j,(r9 "/\" s9)} is non empty set
{j} is non empty set
{{j,(r9 "/\" s9)},{j}} is non empty set
the L_meet of L . [j,(r9 "/\" s9)] is set
j "/\" r9 is Element of the carrier of L
the L_meet of L . (j,r9) is Element of the carrier of L
[j,r9] is V33() set
{j,r9} is non empty set
{{j,r9},{j}} is non empty set
the L_meet of L . [j,r9] is set
(j "/\" r9) "/\" s9 is Element of the carrier of L
the L_meet of L . ((j "/\" r9),s9) is Element of the carrier of L
[(j "/\" r9),s9] is V33() set
{(j "/\" r9),s9} is non empty set
{(j "/\" r9)} is non empty set
{{(j "/\" r9),s9},{(j "/\" r9)}} is non empty set
the L_meet of L . [(j "/\" r9),s9] is set
the L_meet of L . ((a "/\" b),c) is set
the L_meet of L . [(a "/\" b),c] is set
a is Element of the carrier of FI
b is Element of the carrier of FI
a "\/" b is Element of the carrier of FI
the L_join of FI . (a,b) is Element of the carrier of FI
[a,b] is V33() set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
the L_join of FI . [a,b] is set
a "/\" (a "\/" b) is Element of the carrier of FI
the L_meet of FI . (a,(a "\/" b)) is Element of the carrier of FI
[a,(a "\/" b)] is V33() set
{a,(a "\/" b)} is non empty set
{{a,(a "\/" b)},{a}} is non empty set
the L_meet of FI . [a,(a "\/" b)] is set
the L_meet of L . (a,(a "\/" b)) is set
the L_meet of L . [a,(a "\/" b)] is set
c is Element of x
j is Element of x
c "\/" j is Element of the carrier of L
the L_join of L . (c,j) is Element of the carrier of L
[c,j] is V33() set
{c,j} is non empty set
{c} is non empty set
{{c,j},{c}} is non empty set
the L_join of L . [c,j] is set
c "/\" (c "\/" j) is Element of the carrier of L
the L_meet of L . (c,(c "\/" j)) is Element of the carrier of L
[c,(c "\/" j)] is V33() set
{c,(c "\/" j)} is non empty set
{{c,(c "\/" j)},{c}} is non empty set
the L_meet of L . [c,(c "\/" j)] is set
a is Element of the carrier of FI
b is Element of the carrier of FI
a "/\" b is Element of the carrier of FI
the L_meet of FI . (a,b) is Element of the carrier of FI
[a,b] is V33() set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
the L_meet of FI . [a,b] is set
b "/\" a is Element of the carrier of FI
the L_meet of FI . (b,a) is Element of the carrier of FI
[b,a] is V33() set
{b,a} is non empty set
{b} is non empty set
{{b,a},{b}} is non empty set
the L_meet of FI . [b,a] is set
c is Element of x
j is Element of x
the L_meet of L . (c,j) is Element of the carrier of L
[c,j] is V33() set
{c,j} is non empty set
{c} is non empty set
{{c,j},{c}} is non empty set
the L_meet of L . [c,j] is set
j "/\" c is Element of the carrier of L
the L_meet of L . (j,c) is Element of the carrier of L
[j,c] is V33() set
{j,c} is non empty set
{j} is non empty set
{{j,c},{j}} is non empty set
the L_meet of L . [j,c] is set
a is Element of the carrier of FI
b is Element of the carrier of FI
a "/\" b is Element of the carrier of FI
the L_meet of FI . (a,b) is Element of the carrier of FI
[a,b] is V33() set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
the L_meet of FI . [a,b] is set
(a "/\" b) "\/" b is Element of the carrier of FI
the L_join of FI . ((a "/\" b),b) is Element of the carrier of FI
[(a "/\" b),b] is V33() set
{(a "/\" b),b} is non empty set
{(a "/\" b)} is non empty set
{{(a "/\" b),b},{(a "/\" b)}} is non empty set
the L_join of FI . [(a "/\" b),b] is set
the L_join of L . ((a "/\" b),b) is set
the L_join of L . [(a "/\" b),b] is set
c is Element of x
j is Element of x
c "/\" j is Element of the carrier of L
the L_meet of L . (c,j) is Element of the carrier of L
[c,j] is V33() set
{c,j} is non empty set
{c} is non empty set
{{c,j},{c}} is non empty set
the L_meet of L . [c,j] is set
(c "/\" j) "\/" j is Element of the carrier of L
the L_join of L . ((c "/\" j),j) is Element of the carrier of L
[(c "/\" j),j] is V33() set
{(c "/\" j),j} is non empty set
{(c "/\" j)} is non empty set
{{(c "/\" j),j},{(c "/\" j)}} is non empty set
the L_join of L . [(c "/\" j),j] is set
a is Element of the carrier of FI
b is Element of the carrier of FI
a "\/" b is Element of the carrier of FI
the L_join of FI . (a,b) is Element of the carrier of FI
[a,b] is V33() set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
the L_join of FI . [a,b] is set
b "\/" a is Element of the carrier of FI
the L_join of FI . (b,a) is Element of the carrier of FI
[b,a] is V33() set
{b,a} is non empty set
{b} is non empty set
{{b,a},{b}} is non empty set
the L_join of FI . [b,a] is set
c is Element of x
j is Element of x
the L_join of L . (c,j) is Element of the carrier of L
[c,j] is V33() set
{c,j} is non empty set
{c} is non empty set
{{c,j},{c}} is non empty set
the L_join of L . [c,j] is set
j "\/" c is Element of the carrier of L
the L_join of L . (j,c) is Element of the carrier of L
[j,c] is V33() set
{j,c} is non empty set
{j} is non empty set
{{j,c},{j}} is non empty set
the L_join of L . [j,c] is set
a is Element of the carrier of FI
b is Element of the carrier of FI
c is Element of the carrier of FI
b "\/" c is Element of the carrier of FI
the L_join of FI . (b,c) is Element of the carrier of FI
[b,c] is V33() set
{b,c} is non empty set
{b} is non empty set
{{b,c},{b}} is non empty set
the L_join of FI . [b,c] is set
a "\/" (b "\/" c) is Element of the carrier of FI
the L_join of FI . (a,(b "\/" c)) is Element of the carrier of FI
[a,(b "\/" c)] is V33() set
{a,(b "\/" c)} is non empty set
{a} is non empty set
{{a,(b "\/" c)},{a}} is non empty set
the L_join of FI . [a,(b "\/" c)] is set
a "\/" b is Element of the carrier of FI
the L_join of FI . (a,b) is Element of the carrier of FI
[a,b] is V33() set
{a,b} is non empty set
{{a,b},{a}} is non empty set
the L_join of FI . [a,b] is set
(a "\/" b) "\/" c is Element of the carrier of FI
the L_join of FI . ((a "\/" b),c) is Element of the carrier of FI
[(a "\/" b),c] is V33() set
{(a "\/" b),c} is non empty set
{(a "\/" b)} is non empty set
{{(a "\/" b),c},{(a "\/" b)}} is non empty set
the L_join of FI . [(a "\/" b),c] is set
the L_join of L . (a,(b "\/" c)) is set
the L_join of L . [a,(b "\/" c)] is set
j is Element of x
r9 is Element of x
s9 is Element of x
r9 "\/" s9 is Element of the carrier of L
the L_join of L . (r9,s9) is Element of the carrier of L
[r9,s9] is V33() set
{r9,s9} is non empty set
{r9} is non empty set
{{r9,s9},{r9}} is non empty set
the L_join of L . [r9,s9] is set
j "\/" (r9 "\/" s9) is Element of the carrier of L
the L_join of L . (j,(r9 "\/" s9)) is Element of the carrier of L
[j,(r9 "\/" s9)] is V33() set
{j,(r9 "\/" s9)} is non empty set
{j} is non empty set
{{j,(r9 "\/" s9)},{j}} is non empty set
the L_join of L . [j,(r9 "\/" s9)] is set
j "\/" r9 is Element of the carrier of L
the L_join of L . (j,r9) is Element of the carrier of L
[j,r9] is V33() set
{j,r9} is non empty set
{{j,r9},{j}} is non empty set
the L_join of L . [j,r9] is set
(j "\/" r9) "\/" s9 is Element of the carrier of L
the L_join of L . ((j "\/" r9),s9) is Element of the carrier of L
[(j "\/" r9),s9] is V33() set
{(j "\/" r9),s9} is non empty set
{(j "\/" r9)} is non empty set
{{(j "\/" r9),s9},{(j "\/" r9)}} is non empty set
the L_join of L . [(j "\/" r9),s9] is set
the L_join of L . ((a "\/" b),c) is set
the L_join of L . [(a "\/" b),c] is set
a is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
x is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
[:x,x:] is non empty set
[:[:x,x:],x:] is non empty set
bool [:[:x,x:],x:] 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 V36([: 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_join of L || x is set
the L_join of L | [:x,x:] is Relation-like 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 V36([: 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 L_meet of L || x is set
the L_meet of L | [:x,x:] is Relation-like set
y is Relation-like [:x,x:] -defined x -valued Function-like V36([:x,x:],x) Element of bool [:[:x,x:],x:]
z is Relation-like [:x,x:] -defined x -valued Function-like V36([:x,x:],x) Element of bool [:[:x,x:],x:]
LattStr(# x,y,z #) 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
(L) is non empty final meet-closed join-closed Element of bool the carrier of L
the carrier of L is non empty set
bool the carrier of L is non empty set
(L,(L)) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
[: 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 V36([: 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:], 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
dom the L_meet of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
bool [: the carrier of L, the carrier of L:] is non empty set
the L_meet of L || the carrier of L is set
the L_meet of L | [: the carrier of L, the carrier of L:] is Relation-like 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 V36([: 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:]
dom the L_join of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
the L_join of L || the carrier of L is set
the L_join of L | [: the carrier of L, the carrier of L:] is Relation-like 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
the L_join of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V36([: 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 V36([: 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:]
x is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of (L,x) is non empty set
the L_join of (L,x) is Relation-like [: the carrier of (L,x), the carrier of (L,x):] -defined the carrier of (L,x) -valued Function-like V36([: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x)) Element of bool [:[: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x):]
[: the carrier of (L,x), the carrier of (L,x):] is non empty set
[:[: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x):] is non empty set
bool [:[: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x):] is non empty set
the L_join of L || x is set
[:x,x:] is non empty set
the L_join of L | [:x,x:] is Relation-like set
the L_meet of (L,x) is Relation-like [: the carrier of (L,x), the carrier of (L,x):] -defined the carrier of (L,x) -valued Function-like V36([: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x)) Element of bool [:[: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x):]
the L_meet of L || x is set
the L_meet of L | [:x,x:] is Relation-like set
[:[:x,x:],x:] is non empty set
bool [:[:x,x:],x:] is non empty set
y is Relation-like [:x,x:] -defined x -valued Function-like V36([:x,x:],x) Element of bool [:[:x,x:],x:]
z is Relation-like [:x,x:] -defined x -valued Function-like V36([:x,x:],x) Element of bool [:[:x,x:],x:]
LattStr(# x,y,z #) is non empty strict LattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
x "\/" y 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 V36([: 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_join of L . (x,y) is Element of the carrier of L
[x,y] is V33() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the L_join of L . [x,y] is set
x "/\" y 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 V36([: 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 L_meet of L . (x,y) is Element of the carrier of L
the L_meet of L . [x,y] is set
z is non empty final meet-closed join-closed Element of bool the carrier of L
(L,z) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of (L,z) is non empty set
j is Element of the carrier of (L,z)
k is Element of the carrier of (L,z)
j "\/" k is Element of the carrier of (L,z)
the L_join of (L,z) is Relation-like [: the carrier of (L,z), the carrier of (L,z):] -defined the carrier of (L,z) -valued Function-like V36([: the carrier of (L,z), the carrier of (L,z):], the carrier of (L,z)) Element of bool [:[: the carrier of (L,z), the carrier of (L,z):], the carrier of (L,z):]
[: the carrier of (L,z), the carrier of (L,z):] is non empty set
[:[: the carrier of (L,z), the carrier of (L,z):], the carrier of (L,z):] is non empty set
bool [:[: the carrier of (L,z), the carrier of (L,z):], the carrier of (L,z):] is non empty set
the L_join of (L,z) . (j,k) is Element of the carrier of (L,z)
[j,k] is V33() set
{j,k} is non empty set
{j} is non empty set
{{j,k},{j}} is non empty set
the L_join of (L,z) . [j,k] is set
j "/\" k is Element of the carrier of (L,z)
the L_meet of (L,z) is Relation-like [: the carrier of (L,z), the carrier of (L,z):] -defined the carrier of (L,z) -valued Function-like V36([: the carrier of (L,z), the carrier of (L,z):], the carrier of (L,z)) Element of bool [:[: the carrier of (L,z), the carrier of (L,z):], the carrier of (L,z):]
the L_meet of (L,z) . (j,k) is Element of the carrier of (L,z)
the L_meet of (L,z) . [j,k] is set
[:z,z:] is non empty set
[:[:z,z:],z:] is non empty set
bool [:[:z,z:],z:] is non empty set
the L_join of L || z is set
the L_join of L | [:z,z:] is Relation-like set
the L_meet of L || z is set
the L_meet of L | [:z,z:] is Relation-like set
FI is Relation-like [:z,z:] -defined z -valued Function-like V36([:z,z:],z) Element of bool [:[:z,z:],z:]
a is Relation-like [:z,z:] -defined z -valued Function-like V36([:z,z:],z) Element of bool [:[:z,z:],z:]
LattStr(# z,FI,a #) is non empty strict LattStr
dom FI is Relation-like z -defined z -valued Element of bool [:z,z:]
bool [:z,z:] is non empty set
[:z,z:] is non empty Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
bool [: the carrier of L, the carrier of L:] is non empty set
[x,y] is V33() Element of [: the carrier of L, the carrier of L:]
dom a is Relation-like z -defined z -valued Element of bool [:z,z:]
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
x is Element of the carrier of L
y is Element of the carrier of L
z is non empty final meet-closed join-closed Element of bool the carrier of L
(L,z) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of (L,z) is non empty set
j is Element of the carrier of (L,z)
k is Element of the carrier of (L,z)
x "\/" y 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 V36([: 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_join of L . (x,y) is Element of the carrier of L
[x,y] is V33() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the L_join of L . [x,y] is set
j "\/" k is Element of the carrier of (L,z)
the L_join of (L,z) is Relation-like [: the carrier of (L,z), the carrier of (L,z):] -defined the carrier of (L,z) -valued Function-like V36([: the carrier of (L,z), the carrier of (L,z):], the carrier of (L,z)) Element of bool [:[: the carrier of (L,z), the carrier of (L,z):], the carrier of (L,z):]
[: the carrier of (L,z), the carrier of (L,z):] is non empty set
[:[: the carrier of (L,z), the carrier of (L,z):], the carrier of (L,z):] is non empty set
bool [:[: the carrier of (L,z), the carrier of (L,z):], the carrier of (L,z):] is non empty set
the L_join of (L,z) . (j,k) is Element of the carrier of (L,z)
[j,k] is V33() set
{j,k} is non empty set
{j} is non empty set
{{j,k},{j}} is non empty set
the L_join of (L,z) . [j,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
x is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
y is Element of the carrier of L
z is Element of the carrier of L
[:x,x:] is non empty set
[:[:x,x:],x:] is non empty set
bool [:[:x,x:],x:] 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 V36([: 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_join of L || x is set
the L_join of L | [:x,x:] is Relation-like 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 V36([: 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 L_meet of L || x is set
the L_meet of L | [:x,x:] is Relation-like set
y "\/" z is Element of the carrier of L
the L_join of L . (y,z) is Element of the carrier of L
[y,z] is V33() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the L_join of L . [y,z] is set
the carrier of (L,x) is non empty set
k is Relation-like [:x,x:] -defined x -valued Function-like V36([:x,x:],x) Element of bool [:[:x,x:],x:]
FI is Relation-like [:x,x:] -defined x -valued Function-like V36([:x,x:],x) Element of bool [:[:x,x:],x:]
LattStr(# x,k,FI #) is non empty strict LattStr
j is Element of the carrier of (L,x)
k is Element of the carrier of (L,x)
j "\/" k is Element of the carrier of (L,x)
the L_join of (L,x) is Relation-like [: the carrier of (L,x), the carrier of (L,x):] -defined the carrier of (L,x) -valued Function-like V36([: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x)) Element of bool [:[: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x):]
[: the carrier of (L,x), the carrier of (L,x):] is non empty set
[:[: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x):] is non empty set
bool [:[: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x):] is non empty set
the L_join of (L,x) . (j,k) is Element of the carrier of (L,x)
[j,k] is V33() set
{j,k} is non empty set
{j} is non empty set
{{j,k},{j}} is non empty set
the L_join of (L,x) . [j,k] is set
k "\/" j is Element of the carrier of (L,x)
the L_join of (L,x) . (k,j) is Element of the carrier of (L,x)
[k,j] is V33() set
{k,j} is non empty set
{k} is non empty set
{{k,j},{k}} is non empty set
the L_join of (L,x) . [k,j] is set
a is Relation-like [:x,x:] -defined x -valued Function-like V36([:x,x:],x) Element of bool [:[:x,x:],x:]
b is Relation-like [:x,x:] -defined x -valued Function-like V36([:x,x:],x) Element of bool [:[:x,x:],x:]
LattStr(# x,a,b #) is non empty strict LattStr
j "\/" k is Element of the carrier of (L,x)
FI is Element of x
y "\/" FI is Element of the carrier of L
the L_join of L . (y,FI) is Element of the carrier of L
[y,FI] is V33() set
{y,FI} is non empty set
{{y,FI},{y}} is non empty set
the L_join of L . [y,FI] 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
x is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of (L,x) is non empty set
y is Element of the carrier of (L,x)
j is Element of the carrier of (L,x)
z is Element of the carrier of (L,x)
z "/\" j is Element of the carrier of (L,x)
the L_meet of (L,x) is Relation-like [: the carrier of (L,x), the carrier of (L,x):] -defined the carrier of (L,x) -valued Function-like V36([: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x)) Element of bool [:[: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x):]
[: the carrier of (L,x), the carrier of (L,x):] is non empty set
[:[: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x):] is non empty set
bool [:[: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x):] is non empty set
the L_meet of (L,x) . (z,j) is Element of the carrier of (L,x)
[z,j] is V33() set
{z,j} is non empty set
{z} is non empty set
{{z,j},{z}} is non empty set
the L_meet of (L,x) . [z,j] is set
y "\/" (z "/\" j) is Element of the carrier of (L,x)
the L_join of (L,x) is Relation-like [: the carrier of (L,x), the carrier of (L,x):] -defined the carrier of (L,x) -valued Function-like V36([: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x)) Element of bool [:[: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x):]
the L_join of (L,x) . (y,(z "/\" j)) is Element of the carrier of (L,x)
[y,(z "/\" j)] is V33() set
{y,(z "/\" j)} is non empty set
{y} is non empty set
{{y,(z "/\" j)},{y}} is non empty set
the L_join of (L,x) . [y,(z "/\" j)] is set
y "\/" z is Element of the carrier of (L,x)
the L_join of (L,x) . (y,z) is Element of the carrier of (L,x)
[y,z] is V33() set
{y,z} is non empty set
{{y,z},{y}} is non empty set
the L_join of (L,x) . [y,z] is set
(y "\/" z) "/\" j is Element of the carrier of (L,x)
the L_meet of (L,x) . ((y "\/" z),j) is Element of the carrier of (L,x)
[(y "\/" z),j] is V33() set
{(y "\/" z),j} is non empty set
{(y "\/" z)} is non empty set
{{(y "\/" z),j},{(y "\/" z)}} is non empty set
the L_meet of (L,x) . [(y "\/" z),j] is set
z "/\" j is Element of the carrier of (L,x)
FI is Element of x
a is Element of x
FI "/\" a 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 V36([: 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 . (FI,a) is Element of the carrier of L
[FI,a] is V33() set
{FI,a} is non empty set
{FI} is non empty set
{{FI,a},{FI}} is non empty set
the L_meet of L . [FI,a] is set
y "\/" (z "/\" j) is Element of the carrier of (L,x)
the L_join of (L,x) . (y,(z "/\" j)) is Element of the carrier of (L,x)
[y,(z "/\" j)] is V33() set
{y,(z "/\" j)} is non empty set
{{y,(z "/\" j)},{y}} is non empty set
the L_join of (L,x) . [y,(z "/\" j)] is set
k is Element of x
k "\/" (FI "/\" a) 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 V36([: 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 L_join of L . (k,(FI "/\" a)) is Element of the carrier of L
[k,(FI "/\" a)] is V33() set
{k,(FI "/\" a)} is non empty set
{k} is non empty set
{{k,(FI "/\" a)},{k}} is non empty set
the L_join of L . [k,(FI "/\" a)] is set
y "\/" z is Element of the carrier of (L,x)
k "\/" FI is Element of the carrier of L
the L_join of L . (k,FI) is Element of the carrier of L
[k,FI] is V33() set
{k,FI} is non empty set
{{k,FI},{k}} is non empty set
the L_join of L . [k,FI] is set
(y "\/" z) "/\" j is Element of the carrier of (L,x)
the L_meet of (L,x) . ((y "\/" z),j) is Element of the carrier of (L,x)
[(y "\/" z),j] is V33() set
{(y "\/" z),j} is non empty set
{(y "\/" z)} is non empty set
{{(y "\/" z),j},{(y "\/" z)}} is non empty set
the L_meet of (L,x) . [(y "\/" z),j] is set
(k "\/" FI) "/\" a is Element of the carrier of L
the L_meet of L . ((k "\/" FI),a) is Element of the carrier of L
[(k "\/" FI),a] is V33() set
{(k "\/" FI),a} is non empty set
{(k "\/" FI)} is non empty set
{{(k "\/" FI),a},{(k "\/" FI)}} is non empty set
the L_meet of L . [(k "\/" FI),a] 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
x is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of (L,x) is non empty set
y is Element of the carrier of (L,x)
z is Element of the carrier of (L,x)
j is Element of the carrier of (L,x)
z "\/" j is Element of the carrier of (L,x)
the L_join of (L,x) is Relation-like [: the carrier of (L,x), the carrier of (L,x):] -defined the carrier of (L,x) -valued Function-like V36([: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x)) Element of bool [:[: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x):]
[: the carrier of (L,x), the carrier of (L,x):] is non empty set
[:[: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x):] is non empty set
bool [:[: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x):] is non empty set
the L_join of (L,x) . (z,j) is Element of the carrier of (L,x)
[z,j] is V33() set
{z,j} is non empty set
{z} is non empty set
{{z,j},{z}} is non empty set
the L_join of (L,x) . [z,j] is set
y "/\" (z "\/" j) is Element of the carrier of (L,x)
the L_meet of (L,x) is Relation-like [: the carrier of (L,x), the carrier of (L,x):] -defined the carrier of (L,x) -valued Function-like V36([: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x)) Element of bool [:[: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x):]
the L_meet of (L,x) . (y,(z "\/" j)) is Element of the carrier of (L,x)
[y,(z "\/" j)] is V33() set
{y,(z "\/" j)} is non empty set
{y} is non empty set
{{y,(z "\/" j)},{y}} is non empty set
the L_meet of (L,x) . [y,(z "\/" j)] is set
y "/\" z is Element of the carrier of (L,x)
the L_meet of (L,x) . (y,z) is Element of the carrier of (L,x)
[y,z] is V33() set
{y,z} is non empty set
{{y,z},{y}} is non empty set
the L_meet of (L,x) . [y,z] is set
y "/\" j is Element of the carrier of (L,x)
the L_meet of (L,x) . (y,j) is Element of the carrier of (L,x)
[y,j] is V33() set
{y,j} is non empty set
{{y,j},{y}} is non empty set
the L_meet of (L,x) . [y,j] is set
(y "/\" z) "\/" (y "/\" j) is Element of the carrier of (L,x)
the L_join of (L,x) . ((y "/\" z),(y "/\" j)) is Element of the carrier of (L,x)
[(y "/\" z),(y "/\" j)] is V33() set
{(y "/\" z),(y "/\" j)} is non empty set
{(y "/\" z)} is non empty set
{{(y "/\" z),(y "/\" j)},{(y "/\" z)}} is non empty set
the L_join of (L,x) . [(y "/\" z),(y "/\" j)] is set
z "\/" j is Element of the carrier of (L,x)
y "/\" z is Element of the carrier of (L,x)
k is Element of x
FI is Element of x
k "/\" FI 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 V36([: 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 . (k,FI) is Element of the carrier of L
[k,FI] is V33() set
{k,FI} is non empty set
{k} is non empty set
{{k,FI},{k}} is non empty set
the L_meet of L . [k,FI] is set
y "/\" j is Element of the carrier of (L,x)
a is Element of x
k "/\" a is Element of the carrier of L
the L_meet of L . (k,a) is Element of the carrier of L
[k,a] is V33() set
{k,a} is non empty set
{{k,a},{k}} is non empty set
the L_meet of L . [k,a] is set
y "/\" (z "\/" j) is Element of the carrier of (L,x)
the L_meet of (L,x) . (y,(z "\/" j)) is Element of the carrier of (L,x)
[y,(z "\/" j)] is V33() set
{y,(z "\/" j)} is non empty set
{{y,(z "\/" j)},{y}} is non empty set
the L_meet of (L,x) . [y,(z "\/" j)] is set
b is Element of x
k "/\" b is Element of the carrier of L
the L_meet of L . (k,b) is Element of the carrier of L
[k,b] is V33() set
{k,b} is non empty set
{{k,b},{k}} is non empty set
the L_meet of L . [k,b] is set
FI "\/" a 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 V36([: 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 L_join of L . (FI,a) is Element of the carrier of L
[FI,a] is V33() set
{FI,a} is non empty set
{FI} is non empty set
{{FI,a},{FI}} is non empty set
the L_join of L . [FI,a] is set
k "/\" (FI "\/" a) is Element of the carrier of L
the L_meet of L . (k,(FI "\/" a)) is Element of the carrier of L
[k,(FI "\/" a)] is V33() set
{k,(FI "\/" a)} is non empty set
{{k,(FI "\/" a)},{k}} is non empty set
the L_meet of L . [k,(FI "\/" a)] is set
(k "/\" FI) "\/" (k "/\" a) is Element of the carrier of L
the L_join of L . ((k "/\" FI),(k "/\" a)) is Element of the carrier of L
[(k "/\" FI),(k "/\" a)] is V33() set
{(k "/\" FI),(k "/\" a)} is non empty set
{(k "/\" FI)} is non empty set
{{(k "/\" FI),(k "/\" a)},{(k "/\" FI)}} is non empty set
the L_join of L . [(k "/\" FI),(k "/\" a)] is set
(y "/\" z) "\/" (y "/\" j) is Element of the carrier of (L,x)
the L_join of (L,x) . ((y "/\" z),(y "/\" j)) is Element of the carrier of (L,x)
[(y "/\" z),(y "/\" j)] is V33() set
{(y "/\" z),(y "/\" j)} is non empty set
{(y "/\" z)} is non empty set
{{(y "/\" z),(y "/\" j)},{(y "/\" z)}} is non empty set
the L_join of (L,x) . [(y "/\" z),(y "/\" j)] 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
x is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
y is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded () LattStr
the carrier of y is non empty set
bool the carrier of y is non empty set
the carrier of (L,x) is non empty set
j is Element of the carrier of (L,x)
k is Element of the carrier of (L,x)
FI is Element of x
a is Element of x
b is Element of the carrier of L
FI "/\" b 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 V36([: 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 . (FI,b) is Element of the carrier of L
[FI,b] is V33() set
{FI,b} is non empty set
{FI} is non empty set
{{FI,b},{FI}} is non empty set
the L_meet of L . [FI,b] is set
c is Element of the carrier of y
j is Element of the carrier of y
(y,c,j) is Element of the carrier of y
z is non empty final meet-closed join-closed Element of bool the carrier of y
r9 is Element of the carrier of (L,x)
j "/\" r9 is Element of the carrier of (L,x)
the L_meet of (L,x) is Relation-like [: the carrier of (L,x), the carrier of (L,x):] -defined the carrier of (L,x) -valued Function-like V36([: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x)) Element of bool [:[: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x):]
[: the carrier of (L,x), the carrier of (L,x):] is non empty set
[:[: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x):] is non empty set
bool [:[: the carrier of (L,x), the carrier of (L,x):], the carrier of (L,x):] is non empty set
the L_meet of (L,x) . (j,r9) is Element of the carrier of (L,x)
[j,r9] is V33() set
{j,r9} is non empty set
{j} is non empty set
{{j,r9},{j}} is non empty set
the L_meet of (L,x) . [j,r9] is set
j "/\" r9 is Element of the carrier of (L,x)
s9 is Element of the carrier of (L,x)
j "/\" s9 is Element of the carrier of (L,x)
the L_meet of (L,x) . (j,s9) is Element of the carrier of (L,x)
[j,s9] is V33() set
{j,s9} is non empty set
{{j,s9},{j}} is non empty set
the L_meet of (L,x) . [j,s9] is set
j "/\" s9 is Element of the carrier of (L,x)
s is Element of x
FI "/\" s is Element of the carrier of L
the L_meet of L . (FI,s) is Element of the carrier of L
[FI,s] is V33() set
{FI,s} is non empty set
{{FI,s},{FI}} is non empty set
the L_meet of L . [FI,s] 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
x is Element of the carrier of L
(L,x) is non empty final meet-closed join-closed Element of bool the carrier of L
bool the carrier of L is non empty set
{ b₁ where b₁ is Element of the carrier of L : x [= b₁ } is set
(L,(L,x)) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of (L,(L,x)) is non empty set
y is Element of the carrier of (L,(L,x))
z is Element of the carrier of (L,(L,x))
y "/\" z is Element of the carrier of (L,(L,x))
the L_meet of (L,(L,x)) is Relation-like [: the carrier of (L,(L,x)), the carrier of (L,(L,x)):] -defined the carrier of (L,(L,x)) -valued Function-like V36([: the carrier of (L,(L,x)), the carrier of (L,(L,x)):], the carrier of (L,(L,x))) Element of bool [:[: the carrier of (L,(L,x)), the carrier of (L,(L,x)):], the carrier of (L,(L,x)):]
[: the carrier of (L,(L,x)), the carrier of (L,(L,x)):] is non empty set
[:[: the carrier of (L,(L,x)), the carrier of (L,(L,x)):], the carrier of (L,(L,x)):] is non empty set
bool [:[: the carrier of (L,(L,x)), the carrier of (L,(L,x)):], the carrier of (L,(L,x)):] is non empty set
the L_meet of (L,(L,x)) . (y,z) is Element of the carrier of (L,(L,x))
[y,z] is V33() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the L_meet of (L,(L,x)) . [y,z] is set
z "/\" y is Element of the carrier of (L,(L,x))
the L_meet of (L,(L,x)) . (z,y) is Element of the carrier of (L,(L,x))
[z,y] is V33() set
{z,y} is non empty set
{z} is non empty set
{{z,y},{z}} is non empty set
the L_meet of (L,(L,x)) . [z,y] is set
j is Element of (L,x)
x "/\" j 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 V36([: 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 . (x,j) is Element of the carrier of L
[x,j] is V33() set
{x,j} is non empty set
{x} is non empty set
{{x,j},{x}} is non empty set
the L_meet of L . [x,j] 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
x is Element of the carrier of L
(L,x) is non empty final meet-closed join-closed Element of bool the carrier of L
bool the carrier of L is non empty set
{ b₁ where b₁ is Element of the carrier of L : x [= b₁ } is set
(L,(L,x)) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
Bottom (L,(L,x)) is Element of the carrier of (L,(L,x))
the carrier of (L,(L,x)) is non empty set
y is Element of the carrier of (L,(L,x))
z is Element of the carrier of (L,(L,x))
y "/\" z is Element of the carrier of (L,(L,x))
the L_meet of (L,(L,x)) is Relation-like [: the carrier of (L,(L,x)), the carrier of (L,(L,x)):] -defined the carrier of (L,(L,x)) -valued Function-like V36([: the carrier of (L,(L,x)), the carrier of (L,(L,x)):], the carrier of (L,(L,x))) Element of bool [:[: the carrier of (L,(L,x)), the carrier of (L,(L,x)):], the carrier of (L,(L,x)):]
[: the carrier of (L,(L,x)), the carrier of (L,(L,x)):] is non empty set
[:[: the carrier of (L,(L,x)), the carrier of (L,(L,x)):], the carrier of (L,(L,x)):] is non empty set
bool [:[: the carrier of (L,(L,x)), the carrier of (L,(L,x)):], the carrier of (L,(L,x)):] is non empty set
the L_meet of (L,(L,x)) . (y,z) is Element of the carrier of (L,(L,x))
[y,z] is V33() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the L_meet of (L,(L,x)) . [y,z] is set
j is Element of (L,x)
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
Top L is Element of the carrier of L
x is Element of the carrier of L
(L,x) is non empty final meet-closed join-closed Element of bool the carrier of L
bool the carrier of L is non empty set
{ b₁ where b₁ is Element of the carrier of L : x [= b₁ } is set
(L,(L,x)) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
Top (L,(L,x)) is Element of the carrier of (L,(L,x))
the carrier of (L,(L,x)) is non empty set
y is Element of the carrier of L
j is Element of the carrier of (L,(L,x))
z is Element of the carrier of (L,(L,x))
j "\/" z is Element of the carrier of (L,(L,x))
the L_join of (L,(L,x)) is Relation-like [: the carrier of (L,(L,x)), the carrier of (L,(L,x)):] -defined the carrier of (L,(L,x)) -valued Function-like V36([: the carrier of (L,(L,x)), the carrier of (L,(L,x)):], the carrier of (L,(L,x))) Element of bool [:[: the carrier of (L,(L,x)), the carrier of (L,(L,x)):], the carrier of (L,(L,x)):]
[: the carrier of (L,(L,x)), the carrier of (L,(L,x)):] is non empty set
[:[: the carrier of (L,(L,x)), the carrier of (L,(L,x)):], the carrier of (L,(L,x)):] is non empty set
bool [:[: the carrier of (L,(L,x)), the carrier of (L,(L,x)):], the carrier of (L,(L,x)):] is non empty set
the L_join of (L,(L,x)) . (j,z) is Element of the carrier of (L,(L,x))
[j,z] is V33() set
{j,z} is non empty set
{j} is non empty set
{{j,z},{j}} is non empty set
the L_join of (L,(L,x)) . [j,z] is set
k is Element of (L,x)
y "\/" 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 V36([: 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_join of L . (y,k) is Element of the carrier of L
[y,k] is V33() set
{y,k} is non empty set
{y} is non empty set
{{y,k},{y}} is non empty set
the L_join of L . [y,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
x is Element of the carrier of L
(L,x) is non empty final meet-closed join-closed Element of bool the carrier of L
bool the carrier of L is non empty set
{ b₁ where b₁ is Element of the carrier of L : x [= b₁ } is set
(L,(L,x)) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
x is Element of the carrier of L
(L,x) is non empty final meet-closed join-closed Element of bool the carrier of L
bool the carrier of L is non empty set
{ b₁ where b₁ is Element of the carrier of L : x [= b₁ } is set
(L,(L,x)) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
z is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
the carrier of z is non empty set
j is Element of the carrier of z
y 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 y is non empty set
k is Element of (L,x)
a is Element of the carrier of L
the carrier of (L,(L,x)) is non empty set
x "\/" a 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 V36([: 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_join of L . (x,a) is Element of the carrier of L
[x,a] is V33() set
{x,a} is non empty set
{x} is non empty set
{{x,a},{x}} is non empty set
the L_join of L . [x,a] is set
b is Element of the carrier of z
b "\/" j is Element of the carrier of z
the L_join of z is Relation-like [: the carrier of z, the carrier of z:] -defined the carrier of z -valued Function-like V36([: the carrier of z, the carrier of z:], the carrier of z) Element of bool [:[: the carrier of z, the carrier of z:], the carrier of z:]
[: the carrier of z, the carrier of z:] is non empty set
[:[: the carrier of z, the carrier of z:], the carrier of z:] is non empty set
bool [:[: the carrier of z, the carrier of z:], the carrier of z:] is non empty set
the L_join of z . (b,j) is Element of the carrier of z
[b,j] is V33() set
{b,j} is non empty set
{b} is non empty set
{{b,j},{b}} is non empty set
the L_join of z . [b,j] is set
(x "\/" a) "\/" k is Element of the carrier of L
the L_join of L . ((x "\/" a),k) is Element of the carrier of L
[(x "\/" a),k] is V33() set
{(x "\/" a),k} is non empty set
{(x "\/" a)} is non empty set
{{(x "\/" a),k},{(x "\/" a)}} is non empty set
the L_join of L . [(x "\/" a),k] is set
a "\/" k is Element of the carrier of L
the L_join of L . (a,k) is Element of the carrier of L
[a,k] is V33() set
{a,k} is non empty set
{a} is non empty set
{{a,k},{a}} is non empty set
the L_join of L . [a,k] is set
x "\/" (a "\/" k) is Element of the carrier of L
the L_join of L . (x,(a "\/" k)) is Element of the carrier of L
[x,(a "\/" k)] is V33() set
{x,(a "\/" k)} is non empty set
{{x,(a "\/" k)},{x}} is non empty set
the L_join of L . [x,(a "\/" k)] is set
FI is Element of the carrier of y
Top y is Element of the carrier of y
FI "\/" (Top y) is Element of the carrier of y
the L_join of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like V36([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the L_join of y . (FI,(Top y)) is Element of the carrier of y
[FI,(Top y)] is V33() set
{FI,(Top y)} is non empty set
{FI} is non empty set
{{FI,(Top y)},{FI}} is non empty set
the L_join of y . [FI,(Top y)] is set
Top L is Element of the carrier of L
Top z is Element of the carrier of z
j "\/" b is Element of the carrier of z
the L_join of z . (j,b) is Element of the carrier of z
[j,b] is V33() set
{j,b} is non empty set
{j} is non empty set
{{j,b},{j}} is non empty set
the L_join of z . [j,b] is set
b "/\" j is Element of the carrier of z
the L_meet of z is Relation-like [: the carrier of z, the carrier of z:] -defined the carrier of z -valued Function-like V36([: the carrier of z, the carrier of z:], the carrier of z) Element of bool [:[: the carrier of z, the carrier of z:], the carrier of z:]
the L_meet of z . (b,j) is Element of the carrier of z
the L_meet of z . [b,j] is set
Bottom z is Element of the carrier of z
j "/\" b is Element of the carrier of z
the L_meet of z . (j,b) is Element of the carrier of z
the L_meet of z . [j,b] is set
j "\/" b is Element of the carrier of z
(x "\/" a) "/\" 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 V36([: 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 L_meet of L . ((x "\/" a),k) is Element of the carrier of L
the L_meet of L . [(x "\/" a),k] is set
a "/\" k is Element of the carrier of L
the L_meet of L . (a,k) is Element of the carrier of L
the L_meet of L . [a,k] is set
x "\/" (a "/\" k) is Element of the carrier of L
the L_join of L . (x,(a "/\" k)) is Element of the carrier of L
[x,(a "/\" k)] is V33() set
{x,(a "/\" k)} is non empty set
{{x,(a "/\" k)},{x}} is non empty set
the L_join of L . [x,(a "/\" k)] is set
b "/\" j is Element of the carrier of z
Bottom y is Element of the carrier of y
FI "\/" (Bottom y) is Element of the carrier of y
the L_join of y . (FI,(Bottom y)) is Element of the carrier of y
[FI,(Bottom y)] is V33() set
{FI,(Bottom y)} is non empty set
{{FI,(Bottom y)},{FI}} is non empty set
the L_join of y . [FI,(Bottom y)] 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
x is Element of the carrier of L
(L,x) is non empty final meet-closed join-closed Element of bool the carrier of L
bool the carrier of L is non empty set
{ b₁ where b₁ is Element of the carrier of L : x [= b₁ } is set
(L,(L,x)) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of L is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
(L,x,y) is Element of the carrier of L
(L,y,x) is Element of the carrier of L
(L,x,y) "/\" (L,y,x) 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 V36([: 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 . ((L,x,y),(L,y,x)) is Element of the carrier of L
[(L,x,y),(L,y,x)] is V33() set
{(L,x,y),(L,y,x)} is non empty set
{(L,x,y)} is non empty set
{{(L,x,y),(L,y,x)},{(L,x,y)}} is non empty set
the L_meet of L . [(L,x,y),(L,y,x)] 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
x is Element of the carrier of L
y is Element of the carrier of L
(L,x,y) is Element of the carrier of L
(L,x,y) is Element of the carrier of L
(L,y,x) is Element of the carrier of L
(L,x,y) "/\" (L,y,x) 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 V36([: 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 . ((L,x,y),(L,y,x)) is Element of the carrier of L
[(L,x,y),(L,y,x)] is V33() set
{(L,x,y),(L,y,x)} is non empty set
{(L,x,y)} is non empty set
{{(L,x,y),(L,y,x)},{(L,x,y)}} is non empty set
the L_meet of L . [(L,x,y),(L,y,x)] is set
(L,y,x) is Element of the carrier of L
(L,y,x) "/\" (L,x,y) is Element of the carrier of L
the L_meet of L . ((L,y,x),(L,x,y)) is Element of the carrier of L
[(L,y,x),(L,x,y)] is V33() set
{(L,y,x),(L,x,y)} is non empty set
{(L,y,x)} is non empty set
{{(L,y,x),(L,x,y)},{(L,y,x)}} is non empty set
the L_meet of L . [(L,y,x),(L,x,y)] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded () LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
(L,x,y) is Element of the carrier of L
(L,x,y) is Element of the carrier of L
(L,y,x) is Element of the carrier of L
(L,x,y) "/\" (L,y,x) 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 V36([: 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 . ((L,x,y),(L,y,x)) is Element of the carrier of L
[(L,x,y),(L,y,x)] is V33() set
{(L,x,y),(L,y,x)} is non empty set
{(L,x,y)} is non empty set
{{(L,x,y),(L,y,x)},{(L,x,y)}} is non empty set
the L_meet of L . [(L,x,y),(L,y,x)] is set
z is Element of the carrier of L
(L,y,z) is Element of the carrier of L
(L,y,z) is Element of the carrier of L
(L,z,y) is Element of the carrier of L
(L,y,z) "/\" (L,z,y) is Element of the carrier of L
the L_meet of L . ((L,y,z),(L,z,y)) is Element of the carrier of L
[(L,y,z),(L,z,y)] is V33() set
{(L,y,z),(L,z,y)} is non empty set
{(L,y,z)} is non empty set
{{(L,y,z),(L,z,y)},{(L,y,z)}} is non empty set
the L_meet of L . [(L,y,z),(L,z,y)] is set
(L,x,z) is Element of the carrier of L
(L,x,z) is Element of the carrier of L
(L,z,x) is Element of the carrier of L
(L,x,z) "/\" (L,z,x) is Element of the carrier of L
the L_meet of L . ((L,x,z),(L,z,x)) is Element of the carrier of L
[(L,x,z),(L,z,x)] is V33() set
{(L,x,z),(L,z,x)} is non empty set
{(L,x,z)} is non empty set
{{(L,x,z),(L,z,x)},{(L,x,z)}} is non empty set
the L_meet of L . [(L,x,z),(L,z,x)] is set
j 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
bool the carrier of L is non empty set
x is non empty final meet-closed join-closed Element of bool the carrier of L
y is Relation-like set
field y is set
proj1 y is set
rng y is set
(proj1 y) \/ (rng y) is set
z is set
j is set
[z,j] is V33() set
{z,j} is non empty set
{z} is non empty set
{{z,j},{z}} is non empty set
k is set
[k,z] is V33() set
{k,z} is non empty set
{k} is non empty set
{{k,z},{k}} is non empty set
z is Element of the carrier of L
j is Element of the carrier of L
[z,j] is V33() Element of [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
{z,j} is non empty set
{z} is non empty set
{{z,j},{z}} is non empty set
(L,z,j) is Element of the carrier of L
(L,z,j) is Element of the carrier of L
(L,j,z) is Element of the carrier of L
(L,z,j) "/\" (L,j,z) 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 V36([: 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:], 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 . ((L,z,j),(L,j,z)) is Element of the carrier of L
[(L,z,j),(L,j,z)] is V33() set
{(L,z,j),(L,j,z)} is non empty set
{(L,z,j)} is non empty set
{{(L,z,j),(L,j,z)},{(L,z,j)}} is non empty set
the L_meet of L . [(L,z,j),(L,j,z)] is set
k is Element of the carrier of L
FI is Element of the carrier of L
(L,k,FI) is Element of the carrier of L
(L,k,FI) is Element of the carrier of L
(L,FI,k) is Element of the carrier of L
(L,k,FI) "/\" (L,FI,k) is Element of the carrier of L
the L_meet of L . ((L,k,FI),(L,FI,k)) is Element of the carrier of L
[(L,k,FI),(L,FI,k)] is V33() set
{(L,k,FI),(L,FI,k)} is non empty set
{(L,k,FI)} is non empty set
{{(L,k,FI),(L,FI,k)},{(L,k,FI)}} is non empty set
the L_meet of L . [(L,k,FI),(L,FI,k)] is set
y is Relation-like set
field y is set
proj1 y is set
rng y is set
(proj1 y) \/ (rng y) is set
z is Relation-like set
field z is set
proj1 z is set
rng z is set
(proj1 z) \/ (rng z) is set
j is set
k is set
[j,k] is V33() set
{j,k} is non empty set
{j} is non empty set
{{j,k},{j}} is non empty set
FI is Element of the carrier of L
a is Element of the carrier of L
(L,FI,a) is Element of the carrier of L
(L,FI,a) is Element of the carrier of L
(L,a,FI) is Element of the carrier of L
(L,FI,a) "/\" (L,a,FI) 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 V36([: 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 . ((L,FI,a),(L,a,FI)) is Element of the carrier of L
[(L,FI,a),(L,a,FI)] is V33() set
{(L,FI,a),(L,a,FI)} is non empty set
{(L,FI,a)} is non empty set
{{(L,FI,a),(L,a,FI)},{(L,FI,a)}} is non empty set
the L_meet of L . [(L,FI,a),(L,a,FI)] is set
FI is Element of the carrier of L
a is Element of the carrier of L
(L,FI,a) is Element of the carrier of L
(L,FI,a) is Element of the carrier of L
(L,a,FI) is Element of the carrier of L
(L,FI,a) "/\" (L,a,FI) 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 V36([: 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 . ((L,FI,a),(L,a,FI)) is Element of the carrier of L
[(L,FI,a),(L,a,FI)] is V33() set
{(L,FI,a),(L,a,FI)} is non empty set
{(L,FI,a)} is non empty set
{{(L,FI,a),(L,a,FI)},{(L,FI,a)}} is non empty set
the L_meet of L . [(L,FI,a),(L,a,FI)] 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
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
x is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x) is Relation-like set
y is set
z is set
[y,z] is V33() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
field (L,x) is set
proj1 (L,x) is set
rng (L,x) is set
(proj1 (L,x)) \/ (rng (L,x)) 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
x is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x) is Relation-like set
y is set
[y,y] is V33() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
z is Element of the carrier of L
(L,z,z) is Element of the carrier of L
Top L is Element of the carrier of L
(L,z,z) is Element of the carrier of L
(L,z,z) "/\" (L,z,z) 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 V36([: 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 . ((L,z,z),(L,z,z)) is Element of the carrier of L
[(L,z,z),(L,z,z)] is V33() set
{(L,z,z),(L,z,z)} is non empty set
{(L,z,z)} is non empty set
{{(L,z,z),(L,z,z)},{(L,z,z)}} is non empty set
the L_meet of L . [(L,z,z),(L,z,z)] 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
x is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x) is Relation-like set
y is set
z is set
[y,z] is V33() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
[z,y] is V33() set
{z,y} is non empty set
{z} is non empty set
{{z,y},{z}} is non empty set
j is Element of the carrier of L
k is Element of the carrier of L
(L,j,k) is Element of the carrier of L
(L,j,k) is Element of the carrier of L
(L,k,j) is Element of the carrier of L
(L,j,k) "/\" (L,k,j) 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 V36([: 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 . ((L,j,k),(L,k,j)) is Element of the carrier of L
[(L,j,k),(L,k,j)] is V33() set
{(L,j,k),(L,k,j)} is non empty set
{(L,j,k)} is non empty set
{{(L,j,k),(L,k,j)},{(L,j,k)}} is non empty set
the L_meet of L . [(L,j,k),(L,k,j)] is set
(L,k,j) is Element of the carrier of L
(L,k,j) "/\" (L,j,k) is Element of the carrier of L
the L_meet of L . ((L,k,j),(L,j,k)) is Element of the carrier of L
[(L,k,j),(L,j,k)] is V33() set
{(L,k,j),(L,j,k)} is non empty set
{(L,k,j)} is non empty set
{{(L,k,j),(L,j,k)},{(L,k,j)}} is non empty set
the L_meet of L . [(L,k,j),(L,j,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
x is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x) is Relation-like set
y is set
z is set
[y,z] is V33() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
j is set
[z,j] is V33() set
{z,j} is non empty set
{z} is non empty set
{{z,j},{z}} is non empty set
[y,j] is V33() set
{y,j} is non empty set
{{y,j},{y}} is non empty set
k is Element of the carrier of L
FI is Element of the carrier of L
(L,k,FI) is Element of the carrier of L
(L,k,FI) is Element of the carrier of L
(L,FI,k) is Element of the carrier of L
(L,k,FI) "/\" (L,FI,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 V36([: 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 . ((L,k,FI),(L,FI,k)) is Element of the carrier of L
[(L,k,FI),(L,FI,k)] is V33() set
{(L,k,FI),(L,FI,k)} is non empty set
{(L,k,FI)} is non empty set
{{(L,k,FI),(L,FI,k)},{(L,k,FI)}} is non empty set
the L_meet of L . [(L,k,FI),(L,FI,k)] is set
a is Element of the carrier of L
(L,FI,a) is Element of the carrier of L
(L,FI,a) is Element of the carrier of L
(L,a,FI) is Element of the carrier of L
(L,FI,a) "/\" (L,a,FI) is Element of the carrier of L
the L_meet of L . ((L,FI,a),(L,a,FI)) is Element of the carrier of L
[(L,FI,a),(L,a,FI)] is V33() set
{(L,FI,a),(L,a,FI)} is non empty set
{(L,FI,a)} is non empty set
{{(L,FI,a),(L,a,FI)},{(L,FI,a)}} is non empty set
the L_meet of L . [(L,FI,a),(L,a,FI)] is set
(L,k,a) is Element of the carrier of L
(L,k,a) is Element of the carrier of L
(L,a,k) is Element of the carrier of L
(L,k,a) "/\" (L,a,k) is Element of the carrier of L
the L_meet of L . ((L,k,a),(L,a,k)) is Element of the carrier of L
[(L,k,a),(L,a,k)] is V33() set
{(L,k,a),(L,a,k)} is non empty set
{(L,k,a)} is non empty set
{{(L,k,a),(L,a,k)},{(L,k,a)}} is non empty set
the L_meet of L . [(L,k,a),(L,a,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
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
x is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x) is Relation-like set
y is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
field y is set
proj1 y is set
rng y is set
(proj1 y) \/ (rng y) is set
dom y is 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
bool the carrier of L is non empty set
x is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x) is Relation-like set
field (L,x) is set
proj1 (L,x) is set
rng (L,x) is set
(proj1 (L,x)) \/ (rng (L,x)) is set
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, 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 distributive modular upper-bounded () LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
x is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x) is Relation-like set
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, 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 distributive modular lower-bounded upper-bounded bounded complemented Boolean () LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
x is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x) is Relation-like set
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, 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
the carrier of L is non empty set
bool 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
the carrier of L is non empty set
bool the carrier of L is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
[x,y] is V33() Element of [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
z is non empty final meet-closed join-closed Element of bool the carrier of L
(L,z) is Relation-like set
(L,x,y) is Element of the carrier of L
(L,x,y) is Element of the carrier of L
(L,y,x) is Element of the carrier of L
(L,x,y) "/\" (L,y,x) 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 V36([: 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:], 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 . ((L,x,y),(L,y,x)) is Element of the carrier of L
[(L,x,y),(L,y,x)] is V33() set
{(L,x,y),(L,y,x)} is non empty set
{(L,x,y)} is non empty set
{{(L,x,y),(L,y,x)},{(L,x,y)}} is non empty set
the L_meet of L . [(L,x,y),(L,y,x)] 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 () LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
x is non empty final meet-closed join-closed Element of bool the carrier of L
y is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded () LattStr
the carrier of y is non empty set
bool the carrier of y is non empty set
z is Element of the carrier of y
j is non empty final meet-closed join-closed Element of bool the carrier of y
k is Element of the carrier of L
(L,k,k) is Element of the carrier of L
Top L is Element of the carrier of L
(y,z,z) is Element of the carrier of y
Top y is Element of the carrier of y
(Top y) "/\" (Top y) is Element of the carrier of y
the L_meet of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like V36([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the L_meet of y . ((Top y),(Top y)) is Element of the carrier of y
[(Top y),(Top y)] is V33() set
{(Top y),(Top y)} is non empty set
{(Top y)} is non empty set
{{(Top y),(Top y)},{(Top y)}} is non empty set
the L_meet of y . [(Top y),(Top y)] is set
(y,z,z) is Element of the carrier of y
(y,z,z) "/\" (y,z,z) is Element of the carrier of y
the L_meet of y . ((y,z,z),(y,z,z)) is Element of the carrier of y
[(y,z,z),(y,z,z)] is V33() set
{(y,z,z),(y,z,z)} is non empty set
{(y,z,z)} is non empty set
{{(y,z,z),(y,z,z)},{(y,z,z)}} is non empty set
the L_meet of y . [(y,z,z),(y,z,z)] is set
(L,k,k) is Element of the carrier of L
(L,k,k) "/\" (L,k,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 V36([: 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 . ((L,k,k),(L,k,k)) is Element of the carrier of L
[(L,k,k),(L,k,k)] is V33() set
{(L,k,k),(L,k,k)} is non empty set
{(L,k,k)} is non empty set
{{(L,k,k),(L,k,k)},{(L,k,k)}} is non empty set
the L_meet of L . [(L,k,k),(L,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
x is Element of the carrier of L
y is Element of the carrier of L
z is non empty final meet-closed join-closed Element of bool the carrier of L
(L,x,y) is Element of the carrier of L
(L,x,y) is Element of the carrier of L
(L,y,x) is Element of the carrier of L
(L,x,y) "/\" (L,y,x) 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 V36([: 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 . ((L,x,y),(L,y,x)) is Element of the carrier of L
[(L,x,y),(L,y,x)] is V33() set
{(L,x,y),(L,y,x)} is non empty set
{(L,x,y)} is non empty set
{{(L,x,y),(L,y,x)},{(L,x,y)}} is non empty set
the L_meet of L . [(L,x,y),(L,y,x)] is set
(L,y,x) is Element of the carrier of L
(L,y,x) "/\" (L,x,y) is Element of the carrier of L
the L_meet of L . ((L,y,x),(L,x,y)) is Element of the carrier of L
[(L,y,x),(L,x,y)] is V33() set
{(L,y,x),(L,x,y)} is non empty set
{(L,y,x)} is non empty set
{{(L,y,x),(L,x,y)},{(L,y,x)}} is non empty set
the L_meet of L . [(L,y,x),(L,x,y)] 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 () LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
x is non empty final meet-closed join-closed Element of bool the carrier of L
y is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded () LattStr
the carrier of y is non empty set
bool the carrier of y is non empty set
z is Element of the carrier of y
j is Element of the carrier of y
k is Element of the carrier of y
FI is non empty final meet-closed join-closed Element of bool the carrier of y
a is Element of the carrier of L
b is Element of the carrier of L
c is Element of the carrier of L
(y,z,j) is Element of the carrier of y
(y,z,j) is Element of the carrier of y
(y,j,z) is Element of the carrier of y
(y,z,j) "/\" (y,j,z) is Element of the carrier of y
the L_meet of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like V36([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the L_meet of y . ((y,z,j),(y,j,z)) is Element of the carrier of y
[(y,z,j),(y,j,z)] is V33() set
{(y,z,j),(y,j,z)} is non empty set
{(y,z,j)} is non empty set
{{(y,z,j),(y,j,z)},{(y,z,j)}} is non empty set
the L_meet of y . [(y,z,j),(y,j,z)] is set
(y,j,k) is Element of the carrier of y
(y,j,k) is Element of the carrier of y
(y,k,j) is Element of the carrier of y
(y,j,k) "/\" (y,k,j) is Element of the carrier of y
the L_meet of y . ((y,j,k),(y,k,j)) is Element of the carrier of y
[(y,j,k),(y,k,j)] is V33() set
{(y,j,k),(y,k,j)} is non empty set
{(y,j,k)} is non empty set
{{(y,j,k),(y,k,j)},{(y,j,k)}} is non empty set
the L_meet of y . [(y,j,k),(y,k,j)] is set
(y,z,k) is Element of the carrier of y
(y,z,k) is Element of the carrier of y
(y,k,z) is Element of the carrier of y
(y,z,k) "/\" (y,k,z) is Element of the carrier of y
the L_meet of y . ((y,z,k),(y,k,z)) is Element of the carrier of y
[(y,z,k),(y,k,z)] is V33() set
{(y,z,k),(y,k,z)} is non empty set
{(y,z,k)} is non empty set
{{(y,z,k),(y,k,z)},{(y,z,k)}} is non empty set
the L_meet of y . [(y,z,k),(y,k,z)] is set
(L,a,b) is Element of the carrier of L
(L,a,b) is Element of the carrier of L
(L,b,a) is Element of the carrier of L
(L,a,b) "/\" (L,b,a) 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 V36([: 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 . ((L,a,b),(L,b,a)) is Element of the carrier of L
[(L,a,b),(L,b,a)] is V33() set
{(L,a,b),(L,b,a)} is non empty set
{(L,a,b)} is non empty set
{{(L,a,b),(L,b,a)},{(L,a,b)}} is non empty set
the L_meet of L . [(L,a,b),(L,b,a)] is set
(L,b,c) is Element of the carrier of L
(L,b,c) is Element of the carrier of L
(L,c,b) is Element of the carrier of L
(L,b,c) "/\" (L,c,b) is Element of the carrier of L
the L_meet of L . ((L,b,c),(L,c,b)) is Element of the carrier of L
[(L,b,c),(L,c,b)] is V33() set
{(L,b,c),(L,c,b)} is non empty set
{(L,b,c)} is non empty set
{{(L,b,c),(L,c,b)},{(L,b,c)}} is non empty set
the L_meet of L . [(L,b,c),(L,c,b)] is set
(L,a,c) is Element of the carrier of L
(L,a,c) is Element of the carrier of L
(L,c,a) is Element of the carrier of L
(L,a,c) "/\" (L,c,a) is Element of the carrier of L
the L_meet of L . ((L,a,c),(L,c,a)) is Element of the carrier of L
[(L,a,c),(L,c,a)] is V33() set
{(L,a,c),(L,c,a)} is non empty set
{(L,a,c)} is non empty set
{{(L,a,c),(L,c,a)},{(L,a,c)}} is non empty set
the L_meet of L . [(L,a,c),(L,c,a)] is set
L is non empty join-commutative meet-commutative meet-associative meet-absorbing join-absorbing LattStr
the carrier of L is non empty set
z is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
x "/\" y 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 V36([: 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 . (x,y) is Element of the carrier of L
[x,y] is V33() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the L_meet of L . [x,y] is set
L is non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr
the carrier of L is non empty set
x is Element of the carrier of L
z is Element of the carrier of L
y is Element of the carrier of L
x "\/" y 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 V36([: 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_join of L . (x,y) is Element of the carrier of L
[x,y] is V33() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the L_join of L . [x,y] is set