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

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

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

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

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

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

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

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

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

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

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