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