:: BOOLEALG semantic presentation

K87() is set

K19(K87()) is set

1 is set

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

(L,Y,X) is M2( the U1 of L)

X ` is M2( the U1 of L)

Y "/\" (X `) is M2( the U1 of L)

(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the U1 of L is set

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the U1 of L is set

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "\/" Y is M2( the U1 of L)

Z is M2( the U1 of L)

X "/\" (X "\/" Y) is M2( the U1 of L)

X "/\" Z is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

Z is M2( the U1 of L)

X "\/" Z is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

Z is M2( the U1 of L)

(L,X,Z) is M2( the U1 of L)

Z ` is M2( the U1 of L)

X "/\" (Z `) is M2( the U1 of L)

Y "/\" (Z `) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

Z is M2( the U1 of L)

(L,Y,X) is M2( the U1 of L)

X ` is M2( the U1 of L)

Y "/\" (X `) is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

Z is M2( the U1 of L)

Y "\/" Z is M2( the U1 of L)

S1 is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

Z is M2( the U1 of L)

Y "/\" Z is M2( the U1 of L)

S1 is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

Bottom L is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the U1 of L is set

Bottom L is M2( the U1 of L)

X is M2( the U1 of L)

X "/\" X is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the U1 of L is set

Z is M2( the U1 of L)

S1 is M2( the U1 of L)

Z is M2( the U1 of L)

S1 is M2( the U1 of L)

(L,Z,S1) is M2( the U1 of L)

(L,Z,S1) is M2( the U1 of L)

S1 ` is M2( the U1 of L)

Z "/\" (S1 `) is M2( the U1 of L)

(L,S1,Z) is M2( the U1 of L)

Z ` is M2( the U1 of L)

S1 "/\" (Z `) is M2( the U1 of L)

(L,Z,S1) "\/" (L,S1,Z) is M2( the U1 of L)

(L,S1,Z) is M2( the U1 of L)

(L,S1,Z) "\/" (L,Z,S1) is M2( the U1 of L)

Z is M2( the U1 of L)

S1 is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

Z is M2( the U1 of L)

X "/\" Z is M2( the U1 of L)

(X "/\" Y) "\/" (X "/\" Z) is M2( the U1 of L)

Y "\/" Z is M2( the U1 of L)

X "/\" (Y "\/" Z) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr

the U1 of L is set

Bottom L is M2( the U1 of L)

X is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

Z is M2( the U1 of L)

Y "/\" Z is M2( the U1 of L)

Bottom L is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr

the U1 of L is set

Bottom L is M2( the U1 of L)

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "\/" Y is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

Z is M2( the U1 of L)

Y "/\" Z is M2( the U1 of L)

Bottom L is M2( the U1 of L)

X "/\" Z is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

Z is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

Bottom L is M2( the U1 of L)

X "/\" Z is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

Z is M2( the U1 of L)

Y "/\" Z is M2( the U1 of L)

X "/\" (Y "/\" Z) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

X "/\" Z is M2( the U1 of L)

(X "/\" Z) "/\" Y is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(X "/\" Y) "/\" Z is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

Z is M2( the U1 of L)

(L,Y,Z) is M2( the U1 of L)

Z ` is M2( the U1 of L)

Y "/\" (Z `) is M2( the U1 of L)

X "/\" (L,Y,Z) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(X "/\" Y) "/\" (Z `) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr

the U1 of L is set

Bottom L is M2( the U1 of L)

X is M2( the U1 of L)

X "/\" (Bottom L) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

Z is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

Z is M2( the U1 of L)

Y "/\" Z is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr

the U1 of L is set

Bottom L is M2( the U1 of L)

X is M2( the U1 of L)

Y is M2( the U1 of L)

Z is M2( the U1 of L)

Y "/\" Z is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

Z is M2( the U1 of L)

Z "/\" X is M2( the U1 of L)

Z "/\" Y is M2( the U1 of L)

(Z "/\" X) "/\" (Z "/\" Y) is M2( the U1 of L)

Y "/\" Z is M2( the U1 of L)

X "/\" (Y "/\" Z) is M2( the U1 of L)

Z "/\" (X "/\" (Y "/\" Z)) is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(X "/\" Y) "/\" Z is M2( the U1 of L)

Z "/\" ((X "/\" Y) "/\" Z) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

Z "/\" (Bottom L) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

Z is M2( the U1 of L)

Y "\/" Z is M2( the U1 of L)

Y "\/" (X "/\" (Y `)) is M2( the U1 of L)

Y "\/" X is M2( the U1 of L)

Y "\/" (Y `) is M2( the U1 of L)

(Y "\/" X) "/\" (Y "\/" (Y `)) is M2( the U1 of L)

Top L is M2( the U1 of L)

(Y "\/" X) "/\" (Top L) is M2( the U1 of L)

X "\/" Y is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

Z is M2( the U1 of L)

(L,Z,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

Z "/\" (Y `) is M2( the U1 of L)

(L,Z,X) is M2( the U1 of L)

X ` is M2( the U1 of L)

Z "/\" (X `) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

Z is M2( the U1 of L)

(L,Y,Z) is M2( the U1 of L)

Z ` is M2( the U1 of L)

Y "/\" (Z `) is M2( the U1 of L)

S1 is M2( the U1 of L)

(L,X,S1) is M2( the U1 of L)

S1 ` is M2( the U1 of L)

X "/\" (S1 `) is M2( the U1 of L)

(L,Y,S1) is M2( the U1 of L)

Y "/\" (S1 `) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

Z is M2( the U1 of L)

Y "\/" Z is M2( the U1 of L)

(Y "\/" Z) "/\" (Y `) is M2( the U1 of L)

Y "/\" (Y `) is M2( the U1 of L)

Z "/\" (Y `) is M2( the U1 of L)

(Y "/\" (Y `)) "\/" (Z "/\" (Y `)) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

(Bottom L) "\/" (Z "/\" (Y `)) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

X ` is M2( the U1 of L)

Y is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(X "/\" Y) ` is M2( the U1 of L)

Y ` is M2( the U1 of L)

(X `) "\/" (Y `) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

X ` is M2( the U1 of L)

Y is M2( the U1 of L)

X "\/" Y is M2( the U1 of L)

(X "\/" Y) ` is M2( the U1 of L)

Y ` is M2( the U1 of L)

(X `) "/\" (Y `) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

Bottom L is M2( the U1 of L)

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,Y,X) is M2( the U1 of L)

X ` is M2( the U1 of L)

Y "/\" (X `) is M2( the U1 of L)

X "/\" (Y "/\" (X `)) is M2( the U1 of L)

(X `) "/\" X is M2( the U1 of L)

Y "/\" ((X `) "/\" X) is M2( the U1 of L)

Y "/\" (Bottom L) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,Y,X) is M2( the U1 of L)

X ` is M2( the U1 of L)

Y "/\" (X `) is M2( the U1 of L)

X "\/" (L,Y,X) is M2( the U1 of L)

Top L is M2( the U1 of L)

Y "/\" (Top L) is M2( the U1 of L)

X "\/" (X `) is M2( the U1 of L)

Y "/\" (X "\/" (X `)) is M2( the U1 of L)

Y "/\" X is M2( the U1 of L)

(Y "/\" X) "\/" (Y "/\" (X `)) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

Bottom L is M2( the U1 of L)

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

(Y `) ` is M2( the U1 of L)

(Y `) "/\" Y is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

Bottom L is M2( the U1 of L)

X is M2( the U1 of L)

Y is M2( the U1 of L)

Z is M2( the U1 of L)

Y "\/" Z is M2( the U1 of L)

X "/\" Z is M2( the U1 of L)

X "/\" (Y "\/" Z) is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(X "/\" Y) "\/" (Bottom L) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "\/" Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

(L,X,Y) "\/" Y is M2( the U1 of L)

Top L is M2( the U1 of L)

(X "\/" Y) "/\" (Top L) is M2( the U1 of L)

(Y `) "\/" Y is M2( the U1 of L)

(X "\/" Y) "/\" ((Y `) "\/" Y) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "\/" Y is M2( the U1 of L)

(L,X,(X "\/" Y)) is M2( the U1 of L)

(X "\/" Y) ` is M2( the U1 of L)

X "/\" ((X "\/" Y) `) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(L,X,(X "/\" Y)) is M2( the U1 of L)

(X "/\" Y) ` is M2( the U1 of L)

X "/\" ((X "/\" Y) `) is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

X ` is M2( the U1 of L)

(X `) "\/" (Y `) is M2( the U1 of L)

X "/\" ((X `) "\/" (Y `)) is M2( the U1 of L)

X "/\" (X `) is M2( the U1 of L)

(X "/\" (X `)) "\/" (X "/\" (Y `)) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

(Bottom L) "\/" (X "/\" (Y `)) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

Bottom L is M2( the U1 of L)

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

(L,X,Y) "/\" Y is M2( the U1 of L)

(Y `) "/\" Y is M2( the U1 of L)

X "/\" ((Y `) "/\" Y) is M2( the U1 of L)

X "/\" (Bottom L) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,Y,X) is M2( the U1 of L)

X ` is M2( the U1 of L)

Y "/\" (X `) is M2( the U1 of L)

X "\/" (L,Y,X) is M2( the U1 of L)

X "\/" Y is M2( the U1 of L)

X "\/" (X `) is M2( the U1 of L)

(X "\/" Y) "/\" (X "\/" (X `)) is M2( the U1 of L)

Top L is M2( the U1 of L)

(X "\/" Y) "/\" (Top L) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

(X "/\" Y) "\/" (L,X,Y) is M2( the U1 of L)

(X "/\" Y) "\/" X is M2( the U1 of L)

(X "/\" Y) "\/" (Y `) is M2( the U1 of L)

((X "/\" Y) "\/" X) "/\" ((X "/\" Y) "\/" (Y `)) is M2( the U1 of L)

X "/\" ((X "/\" Y) "\/" (Y `)) is M2( the U1 of L)

X "\/" (Y `) is M2( the U1 of L)

Y "\/" (Y `) is M2( the U1 of L)

(X "\/" (Y `)) "/\" (Y "\/" (Y `)) is M2( the U1 of L)

X "/\" ((X "\/" (Y `)) "/\" (Y "\/" (Y `))) is M2( the U1 of L)

Top L is M2( the U1 of L)

(X "\/" (Y `)) "/\" (Top L) is M2( the U1 of L)

X "/\" ((X "\/" (Y `)) "/\" (Top L)) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

Z is M2( the U1 of L)

(L,Y,Z) is M2( the U1 of L)

Z ` is M2( the U1 of L)

Y "/\" (Z `) is M2( the U1 of L)

(L,X,(L,Y,Z)) is M2( the U1 of L)

(L,Y,Z) ` is M2( the U1 of L)

X "/\" ((L,Y,Z) `) is M2( the U1 of L)

X "/\" Z is M2( the U1 of L)

(L,X,Y) "\/" (X "/\" Z) is M2( the U1 of L)

(Z `) ` is M2( the U1 of L)

(Y `) "\/" ((Z `) `) is M2( the U1 of L)

X "/\" ((Y `) "\/" ((Z `) `)) is M2( the U1 of L)

(Y `) "\/" Z is M2( the U1 of L)

X "/\" ((Y `) "\/" Z) is M2( the U1 of L)

(X "/\" (Y `)) "\/" (X "/\" Z) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

(L,X,(L,X,Y)) is M2( the U1 of L)

(L,X,Y) ` is M2( the U1 of L)

X "/\" ((L,X,Y) `) is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

X ` is M2( the U1 of L)

(Y `) ` is M2( the U1 of L)

(X `) "\/" ((Y `) `) is M2( the U1 of L)

X "/\" ((X `) "\/" ((Y `) `)) is M2( the U1 of L)

(X `) "\/" Y is M2( the U1 of L)

X "/\" ((X `) "\/" Y) is M2( the U1 of L)

X "/\" (X `) is M2( the U1 of L)

(X "/\" (X `)) "\/" (X "/\" Y) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

(Bottom L) "\/" (X "/\" Y) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "\/" Y is M2( the U1 of L)

(L,(X "\/" Y),Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

(X "\/" Y) "/\" (Y `) is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

Y "/\" (Y `) is M2( the U1 of L)

(X "/\" (Y `)) "\/" (Y "/\" (Y `)) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

(X "/\" (Y `)) "\/" (Bottom L) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

Bottom L is M2( the U1 of L)

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

X "/\" X is M2( the U1 of L)

X ` is M2( the U1 of L)

(Y `) ` is M2( the U1 of L)

(X `) "\/" ((Y `) `) is M2( the U1 of L)

(X `) "\/" Y is M2( the U1 of L)

X "/\" ((X `) "\/" Y) is M2( the U1 of L)

X "/\" (X `) is M2( the U1 of L)

(X "/\" (X `)) "\/" (X "/\" Y) is M2( the U1 of L)

(Bottom L) "\/" (X "/\" Y) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

Z is M2( the U1 of L)

Y "\/" Z is M2( the U1 of L)

(L,X,(Y "\/" Z)) is M2( the U1 of L)

(Y "\/" Z) ` is M2( the U1 of L)

X "/\" ((Y "\/" Z) `) is M2( the U1 of L)

(L,X,Z) is M2( the U1 of L)

Z ` is M2( the U1 of L)

X "/\" (Z `) is M2( the U1 of L)

(L,X,Y) "/\" (L,X,Z) is M2( the U1 of L)

(Y `) "/\" (Z `) is M2( the U1 of L)

X "/\" ((Y `) "/\" (Z `)) is M2( the U1 of L)

X "/\" X is M2( the U1 of L)

(X "/\" X) "/\" (Y `) is M2( the U1 of L)

((X "/\" X) "/\" (Y `)) "/\" (Z `) is M2( the U1 of L)

X "/\" (X "/\" (Y `)) is M2( the U1 of L)

(X "/\" (X "/\" (Y `))) "/\" (Z `) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

Z is M2( the U1 of L)

Y "/\" Z is M2( the U1 of L)

(L,X,(Y "/\" Z)) is M2( the U1 of L)

(Y "/\" Z) ` is M2( the U1 of L)

X "/\" ((Y "/\" Z) `) is M2( the U1 of L)

(L,X,Z) is M2( the U1 of L)

Z ` is M2( the U1 of L)

X "/\" (Z `) is M2( the U1 of L)

(L,X,Y) "\/" (L,X,Z) is M2( the U1 of L)

(Y `) "\/" (Z `) is M2( the U1 of L)

X "/\" ((Y `) "\/" (Z `)) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

Z is M2( the U1 of L)

(L,Y,Z) is M2( the U1 of L)

Z ` is M2( the U1 of L)

Y "/\" (Z `) is M2( the U1 of L)

X "/\" (L,Y,Z) is M2( the U1 of L)

X "/\" Z is M2( the U1 of L)

(L,(X "/\" Y),(X "/\" Z)) is M2( the U1 of L)

(X "/\" Z) ` is M2( the U1 of L)

(X "/\" Y) "/\" ((X "/\" Z) `) is M2( the U1 of L)

(L,(X "/\" Y),X) is M2( the U1 of L)

X ` is M2( the U1 of L)

(X "/\" Y) "/\" (X `) is M2( the U1 of L)

(L,(X "/\" Y),Z) is M2( the U1 of L)

(X "/\" Y) "/\" (Z `) is M2( the U1 of L)

(L,(X "/\" Y),X) "\/" (L,(X "/\" Y),Z) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

(Bottom L) "\/" (L,(X "/\" Y),Z) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "\/" Y is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(L,(X "\/" Y),(X "/\" Y)) is M2( the U1 of L)

(X "/\" Y) ` is M2( the U1 of L)

(X "\/" Y) "/\" ((X "/\" Y) `) is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

(L,Y,X) is M2( the U1 of L)

X ` is M2( the U1 of L)

Y "/\" (X `) is M2( the U1 of L)

(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)

(X `) "\/" (Y `) is M2( the U1 of L)

(X "\/" Y) "/\" ((X `) "\/" (Y `)) is M2( the U1 of L)

(X "\/" Y) "/\" (X `) is M2( the U1 of L)

(X "\/" Y) "/\" (Y `) is M2( the U1 of L)

((X "\/" Y) "/\" (X `)) "\/" ((X "\/" Y) "/\" (Y `)) is M2( the U1 of L)

X "/\" (X `) is M2( the U1 of L)

(X "/\" (X `)) "\/" (Y "/\" (X `)) is M2( the U1 of L)

((X "/\" (X `)) "\/" (Y "/\" (X `))) "\/" ((X "\/" Y) "/\" (Y `)) is M2( the U1 of L)

Y "/\" (Y `) is M2( the U1 of L)

(X "/\" (Y `)) "\/" (Y "/\" (Y `)) is M2( the U1 of L)

((X "/\" (X `)) "\/" (Y "/\" (X `))) "\/" ((X "/\" (Y `)) "\/" (Y "/\" (Y `))) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

(Bottom L) "\/" (Y "/\" (X `)) is M2( the U1 of L)

((Bottom L) "\/" (Y "/\" (X `))) "\/" ((X "/\" (Y `)) "\/" (Y "/\" (Y `))) is M2( the U1 of L)

(X "/\" (Y `)) "\/" (Bottom L) is M2( the U1 of L)

(Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" (Bottom L)) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

Z is M2( the U1 of L)

(L,(L,X,Y),Z) is M2( the U1 of L)

Z ` is M2( the U1 of L)

(L,X,Y) "/\" (Z `) is M2( the U1 of L)

Y "\/" Z is M2( the U1 of L)

(L,X,(Y "\/" Z)) is M2( the U1 of L)

(Y "\/" Z) ` is M2( the U1 of L)

X "/\" ((Y "\/" Z) `) is M2( the U1 of L)

(Y `) "/\" (Z `) is M2( the U1 of L)

X "/\" ((Y `) "/\" (Z `)) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

(L,Y,X) is M2( the U1 of L)

X ` is M2( the U1 of L)

Y "/\" (X `) is M2( the U1 of L)

(X "/\" (Y `)) "/\" X is M2( the U1 of L)

(X `) "/\" X is M2( the U1 of L)

Y "/\" ((X `) "/\" X) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

Y "/\" (Bottom L) is M2( the U1 of L)

X "/\" X is M2( the U1 of L)

(X "/\" X) "/\" (Y `) is M2( the U1 of L)

(X "/\" (Y `)) "\/" (X `) is M2( the U1 of L)

X "/\" (X `) is M2( the U1 of L)

(X "/\" (X `)) "\/" (X `) is M2( the U1 of L)

X "\/" (X `) is M2( the U1 of L)

(Y `) "\/" (X `) is M2( the U1 of L)

(X "\/" (X `)) "/\" ((Y `) "\/" (X `)) is M2( the U1 of L)

Top L is M2( the U1 of L)

(Top L) "/\" ((Y `) "\/" (X `)) is M2( the U1 of L)

(Y `) "/\" (X `) is M2( the U1 of L)

(X `) ` is M2( the U1 of L)

(Y `) ` is M2( the U1 of L)

(Y `) "/\" Y is M2( the U1 of L)

X "/\" ((Y `) "/\" Y) is M2( the U1 of L)

(Y "/\" (X `)) "/\" Y is M2( the U1 of L)

X "/\" (Bottom L) is M2( the U1 of L)

Y "/\" Y is M2( the U1 of L)

(X `) "/\" (Y "/\" Y) is M2( the U1 of L)

(X `) "/\" Y is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

Bottom L is M2( the U1 of L)

X is M2( the U1 of L)

(L,X,(Bottom L)) is M2( the U1 of L)

(Bottom L) ` is M2( the U1 of L)

X "/\" ((Bottom L) `) is M2( the U1 of L)

Top L is M2( the U1 of L)

X "/\" (Top L) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

X ` is M2( the U1 of L)

Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

(L,X,Y) ` is M2( the U1 of L)

(X `) "\/" Y is M2( the U1 of L)

(Y `) ` is M2( the U1 of L)

(X `) "\/" ((Y `) `) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

Z is M2( the U1 of L)

Y "\/" Z is M2( the U1 of L)

X "/\" (Y "\/" Z) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

X "/\" Z is M2( the U1 of L)

(X "/\" Y) "\/" (X "/\" Z) is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

X "/\" Z is M2( the U1 of L)

(X "/\" Y) "\/" (X "/\" Z) is M2( the U1 of L)

X "/\" (Y "\/" Z) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

X "/\" Z is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(X "/\" Z) "\/" (X "/\" Y) is M2( the U1 of L)

X "/\" (Y "\/" Z) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

(X "/\" Y) "/\" (L,X,Y) is M2( the U1 of L)

(X "/\" Y) "/\" (Y `) is M2( the U1 of L)

((X "/\" Y) "/\" (Y `)) "/\" X is M2( the U1 of L)

Y "/\" (Y `) is M2( the U1 of L)

X "/\" (Y "/\" (Y `)) is M2( the U1 of L)

(X "/\" (Y "/\" (Y `))) "/\" X is M2( the U1 of L)

Bottom L is M2( the U1 of L)

(Bottom L) "/\" X is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

S1 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of S1 is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

Z is M2( the U1 of L)

Y "\/" Z is M2( the U1 of L)

S2 is M2( the U1 of S1)

S3 is M2( the U1 of S1)

S4 is M2( the U1 of S1)

S3 "\/" S4 is M2( the U1 of S1)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

(L,X,Y) "/\" Y is M2( the U1 of L)

(Y `) "/\" Y is M2( the U1 of L)

X "/\" ((Y `) "/\" Y) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

X "/\" (Bottom L) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "\/" Y is M2( the U1 of L)

(L,(X "\/" Y),Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

(X "\/" Y) "/\" (Y `) is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

Bottom L is M2( the U1 of L)

X ` is M2( the U1 of L)

(X `) "\/" (X "/\" Y) is M2( the U1 of L)

(X `) "\/" X is M2( the U1 of L)

(X `) "\/" Y is M2( the U1 of L)

((X `) "\/" X) "/\" ((X `) "\/" Y) is M2( the U1 of L)

Top L is M2( the U1 of L)

(Top L) "/\" ((X `) "\/" Y) is M2( the U1 of L)

((X `) "\/" Y) ` is M2( the U1 of L)

(X `) ` is M2( the U1 of L)

((X `) `) "/\" (Y `) is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

Y "/\" (Y `) is M2( the U1 of L)

(X "/\" (Y `)) "\/" (Y "/\" (Y `)) is M2( the U1 of L)

(X "/\" (Y `)) "\/" (Bottom L) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

X ` is M2( the U1 of L)

Y is M2( the U1 of L)

Y ` is M2( the U1 of L)

(X `) "\/" (Y `) is M2( the U1 of L)

X "\/" Y is M2( the U1 of L)

X "/\" (X `) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

Y "/\" (Y `) is M2( the U1 of L)

(Y `) "/\" ((X `) "\/" (Y `)) is M2( the U1 of L)

(Y `) "/\" X is M2( the U1 of L)

((Y `) "/\" X) "\/" (Bottom L) is M2( the U1 of L)

Y "/\" (X `) is M2( the U1 of L)

(Y "/\" (X `)) "\/" (Y "/\" (Y `)) is M2( the U1 of L)

Y "/\" (X "\/" Y) is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

(X "/\" (X `)) "\/" (X "/\" (Y `)) is M2( the U1 of L)

X "/\" (X "\/" Y) is M2( the U1 of L)

(X `) "/\" ((X `) "\/" (Y `)) is M2( the U1 of L)

(X `) "/\" Y is M2( the U1 of L)

(Bottom L) "\/" ((X `) "/\" Y) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

X ` is M2( the U1 of L)

Y is M2( the U1 of L)

Y ` is M2( the U1 of L)

(X `) "\/" (Y `) is M2( the U1 of L)

X "\/" Y is M2( the U1 of L)

Y "/\" (X `) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

X "\/" (X `) is M2( the U1 of L)

(X "\/" Y) "/\" (X "\/" (X `)) is M2( the U1 of L)

X "\/" (Bottom L) is M2( the U1 of L)

Top L is M2( the U1 of L)

(X "\/" Y) "/\" (Top L) is M2( the U1 of L)

Y "/\" X is M2( the U1 of L)

(Y "/\" X) ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

Y "\/" X is M2( the U1 of L)

Y "\/" (Y `) is M2( the U1 of L)

(Y "\/" X) "/\" (Y "\/" (Y `)) is M2( the U1 of L)

Y "\/" (Bottom L) is M2( the U1 of L)

(Y "\/" X) "/\" (Top L) is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(X "/\" Y) ` is M2( the U1 of L)

(Y `) "\/" Y is M2( the U1 of L)

(Y `) "\/" (X `) is M2( the U1 of L)

((Y `) "\/" Y) "/\" ((Y `) "\/" (X `)) is M2( the U1 of L)

(Y `) "\/" (Bottom L) is M2( the U1 of L)

(Top L) "/\" ((Y `) "\/" (X `)) is M2( the U1 of L)

(X `) "/\" (Y `) is M2( the U1 of L)

((X `) "/\" (Y `)) ` is M2( the U1 of L)

(X `) ` is M2( the U1 of L)

(Y `) ` is M2( the U1 of L)

((X `) `) "\/" ((Y `) `) is M2( the U1 of L)

X "\/" ((Y `) `) is M2( the U1 of L)

(X `) "\/" X is M2( the U1 of L)

((X `) "\/" X) "/\" ((X `) "\/" (Y `)) is M2( the U1 of L)

(X `) "\/" (Bottom L) is M2( the U1 of L)

(Top L) "/\" ((X `) "\/" (Y `)) is M2( the U1 of L)

(Y `) "/\" (X `) is M2( the U1 of L)

((Y `) "/\" (X `)) ` is M2( the U1 of L)

((Y `) `) "\/" ((X `) `) is M2( the U1 of L)

((Y `) `) "\/" X is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

Bottom L is M2( the U1 of L)

X is M2( the U1 of L)

(L,X,(Bottom L)) is M2( the U1 of L)

(L,X,(Bottom L)) is M2( the U1 of L)

(Bottom L) ` is M2( the U1 of L)

X "/\" ((Bottom L) `) is M2( the U1 of L)

(L,(Bottom L),X) is M2( the U1 of L)

X ` is M2( the U1 of L)

(Bottom L) "/\" (X `) is M2( the U1 of L)

(L,X,(Bottom L)) "\/" (L,(Bottom L),X) is M2( the U1 of L)

X "\/" (Bottom L) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

(L,X,X) is M2( the U1 of L)

(L,X,X) is M2( the U1 of L)

X ` is M2( the U1 of L)

X "/\" (X `) is M2( the U1 of L)

(L,X,X) "\/" (L,X,X) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

(L,Y,X) is M2( the U1 of L)

X ` is M2( the U1 of L)

Y "/\" (X `) is M2( the U1 of L)

(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "\/" Y is M2( the U1 of L)

(L,Y,X) is M2( the U1 of L)

X ` is M2( the U1 of L)

Y "/\" (X `) is M2( the U1 of L)

(L,X,(L,Y,X)) is M2( the U1 of L)

(L,X,(L,Y,X)) is M2( the U1 of L)

(L,Y,X) ` is M2( the U1 of L)

X "/\" ((L,Y,X) `) is M2( the U1 of L)

(L,(L,Y,X),X) is M2( the U1 of L)

(L,Y,X) "/\" (X `) is M2( the U1 of L)

(L,X,(L,Y,X)) "\/" (L,(L,Y,X),X) is M2( the U1 of L)

Top L is M2( the U1 of L)

(X "\/" Y) "/\" (Top L) is M2( the U1 of L)

X "\/" (X `) is M2( the U1 of L)

(X "\/" Y) "/\" (X "\/" (X `)) is M2( the U1 of L)

X "\/" (Y "/\" (X `)) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

X "/\" X is M2( the U1 of L)

(X "/\" (Y `)) "\/" (X "/\" X) is M2( the U1 of L)

((X "/\" (Y `)) "\/" (X "/\" X)) "\/" (Y "/\" (X `)) is M2( the U1 of L)

(X `) ` is M2( the U1 of L)

X "/\" ((X `) `) is M2( the U1 of L)

(X "/\" (Y `)) "\/" (X "/\" ((X `) `)) is M2( the U1 of L)

(X `) "/\" (X `) is M2( the U1 of L)

Y "/\" ((X `) "/\" (X `)) is M2( the U1 of L)

((X "/\" (Y `)) "\/" (X "/\" ((X `) `))) "\/" (Y "/\" ((X `) "/\" (X `))) is M2( the U1 of L)

(Y `) "\/" ((X `) `) is M2( the U1 of L)

X "/\" ((Y `) "\/" ((X `) `)) is M2( the U1 of L)

(X "/\" ((Y `) "\/" ((X `) `))) "\/" (Y "/\" ((X `) "/\" (X `))) is M2( the U1 of L)

(Y "/\" (X `)) ` is M2( the U1 of L)

X "/\" ((Y "/\" (X `)) `) is M2( the U1 of L)

(X "/\" ((Y "/\" (X `)) `)) "\/" (Y "/\" ((X `) "/\" (X `))) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(L,X,(X "/\" Y)) is M2( the U1 of L)

(L,X,(X "/\" Y)) is M2( the U1 of L)

(X "/\" Y) ` is M2( the U1 of L)

X "/\" ((X "/\" Y) `) is M2( the U1 of L)

(L,(X "/\" Y),X) is M2( the U1 of L)

X ` is M2( the U1 of L)

(X "/\" Y) "/\" (X `) is M2( the U1 of L)

(L,X,(X "/\" Y)) "\/" (L,(X "/\" Y),X) is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

X "/\" (X `) is M2( the U1 of L)

Y "/\" (X "/\" (X `)) is M2( the U1 of L)

(X "/\" ((X "/\" Y) `)) "\/" (Y "/\" (X "/\" (X `))) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

Y "/\" (Bottom L) is M2( the U1 of L)

(X "/\" ((X "/\" Y) `)) "\/" (Y "/\" (Bottom L)) is M2( the U1 of L)

(X `) "\/" (Y `) is M2( the U1 of L)

X "/\" ((X `) "\/" (Y `)) is M2( the U1 of L)

(X "/\" (X `)) "\/" (X "/\" (Y `)) is M2( the U1 of L)

(Bottom L) "\/" (X "/\" (Y `)) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "\/" Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

(L,Y,X) is M2( the U1 of L)

X ` is M2( the U1 of L)

Y "/\" (X `) is M2( the U1 of L)

(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(L,X,Y) "\/" (X "/\" Y) is M2( the U1 of L)

(L,Y,X) "\/" X is M2( the U1 of L)

(L,X,Y) "\/" (X "/\" Y) is M2( the U1 of L)

(L,Y,X) "\/" ((L,X,Y) "\/" (X "/\" Y)) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

X "\/" Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

(L,Y,X) is M2( the U1 of L)

X ` is M2( the U1 of L)

Y "/\" (X `) is M2( the U1 of L)

(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)

(L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)

(L,X,Y) ` is M2( the U1 of L)

(X "\/" Y) "/\" ((L,X,Y) `) is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(X "/\" (Y `)) ` is M2( the U1 of L)

(Y "/\" (X `)) ` is M2( the U1 of L)

((X "/\" (Y `)) `) "/\" ((Y "/\" (X `)) `) is M2( the U1 of L)

(X "\/" Y) "/\" (((X "/\" (Y `)) `) "/\" ((Y "/\" (X `)) `)) is M2( the U1 of L)

(X `) ` is M2( the U1 of L)

(Y `) "\/" ((X `) `) is M2( the U1 of L)

((X "/\" (Y `)) `) "/\" ((Y `) "\/" ((X `) `)) is M2( the U1 of L)

(X "\/" Y) "/\" (((X "/\" (Y `)) `) "/\" ((Y `) "\/" ((X `) `))) is M2( the U1 of L)

(Y `) ` is M2( the U1 of L)

(X `) "\/" ((Y `) `) is M2( the U1 of L)

((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" ((X `) `)) is M2( the U1 of L)

(X "\/" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" ((X `) `))) is M2( the U1 of L)

(Y `) "\/" X is M2( the U1 of L)

((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" X) is M2( the U1 of L)

(X "\/" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" X)) is M2( the U1 of L)

(X `) "\/" Y is M2( the U1 of L)

((X `) "\/" Y) "/\" ((Y `) "\/" X) is M2( the U1 of L)

(X "\/" Y) "/\" (((X `) "\/" Y) "/\" ((Y `) "\/" X)) is M2( the U1 of L)

(X "\/" Y) "/\" ((X `) "\/" Y) is M2( the U1 of L)

((X "\/" Y) "/\" ((X `) "\/" Y)) "/\" ((Y `) "\/" X) is M2( the U1 of L)

(X "\/" Y) "/\" (X `) is M2( the U1 of L)

(X "\/" Y) "/\" Y is M2( the U1 of L)

((X "\/" Y) "/\" (X `)) "\/" ((X "\/" Y) "/\" Y) is M2( the U1 of L)

(((X "\/" Y) "/\" (X `)) "\/" ((X "\/" Y) "/\" Y)) "/\" ((Y `) "\/" X) is M2( the U1 of L)

((X "\/" Y) "/\" (X `)) "\/" Y is M2( the U1 of L)

(((X "\/" Y) "/\" (X `)) "\/" Y) "/\" ((Y `) "\/" X) is M2( the U1 of L)

X "/\" (X `) is M2( the U1 of L)

(X "/\" (X `)) "\/" (Y "/\" (X `)) is M2( the U1 of L)

((X "/\" (X `)) "\/" (Y "/\" (X `))) "\/" Y is M2( the U1 of L)

(((X "/\" (X `)) "\/" (Y "/\" (X `))) "\/" Y) "/\" ((Y `) "\/" X) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

(Bottom L) "\/" (Y "/\" (X `)) is M2( the U1 of L)

((Bottom L) "\/" (Y "/\" (X `))) "\/" Y is M2( the U1 of L)

(((Bottom L) "\/" (Y "/\" (X `))) "\/" Y) "/\" ((Y `) "\/" X) is M2( the U1 of L)

Y "/\" ((Y `) "\/" X) is M2( the U1 of L)

Y "/\" (Y `) is M2( the U1 of L)

Y "/\" X is M2( the U1 of L)

(Y "/\" (Y `)) "\/" (Y "/\" X) is M2( the U1 of L)

(Bottom L) "\/" (Y "/\" X) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

(L,Y,X) is M2( the U1 of L)

X ` is M2( the U1 of L)

Y "/\" (X `) is M2( the U1 of L)

(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(L,(L,X,Y),(X "/\" Y)) is M2( the U1 of L)

(L,(L,X,Y),(X "/\" Y)) is M2( the U1 of L)

(X "/\" Y) ` is M2( the U1 of L)

(L,X,Y) "/\" ((X "/\" Y) `) is M2( the U1 of L)

(L,(X "/\" Y),(L,X,Y)) is M2( the U1 of L)

(L,X,Y) ` is M2( the U1 of L)

(X "/\" Y) "/\" ((L,X,Y) `) is M2( the U1 of L)

(L,(L,X,Y),(X "/\" Y)) "\/" (L,(X "/\" Y),(L,X,Y)) is M2( the U1 of L)

X "\/" Y is M2( the U1 of L)

(X `) "\/" (Y `) is M2( the U1 of L)

(L,X,Y) "/\" ((X `) "\/" (Y `)) is M2( the U1 of L)

((L,X,Y) "/\" ((X `) "\/" (Y `))) "\/" ((X "/\" Y) "/\" ((L,X,Y) `)) is M2( the U1 of L)

(L,X,Y) "/\" (X `) is M2( the U1 of L)

(L,X,Y) "/\" (Y `) is M2( the U1 of L)

((L,X,Y) "/\" (X `)) "\/" ((L,X,Y) "/\" (Y `)) is M2( the U1 of L)

(((L,X,Y) "/\" (X `)) "\/" ((L,X,Y) "/\" (Y `))) "\/" ((X "/\" Y) "/\" ((L,X,Y) `)) is M2( the U1 of L)

(L,(L,X,Y),X) is M2( the U1 of L)

(L,(L,X,Y),Y) is M2( the U1 of L)

(L,(L,X,Y),X) "\/" (L,(L,X,Y),Y) is M2( the U1 of L)

(X "/\" (Y `)) ` is M2( the U1 of L)

(Y "/\" (X `)) ` is M2( the U1 of L)

((X "/\" (Y `)) `) "/\" ((Y "/\" (X `)) `) is M2( the U1 of L)

(X "/\" Y) "/\" (((X "/\" (Y `)) `) "/\" ((Y "/\" (X `)) `)) is M2( the U1 of L)

((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" ((X "/\" Y) "/\" (((X "/\" (Y `)) `) "/\" ((Y "/\" (X `)) `))) is M2( the U1 of L)

(Y `) ` is M2( the U1 of L)

(X `) "\/" ((Y `) `) is M2( the U1 of L)

((X `) "\/" ((Y `) `)) "/\" ((Y "/\" (X `)) `) is M2( the U1 of L)

(X "/\" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y "/\" (X `)) `)) is M2( the U1 of L)

((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" ((X "/\" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y "/\" (X `)) `))) is M2( the U1 of L)

(X `) ` is M2( the U1 of L)

(Y `) "\/" ((X `) `) is M2( the U1 of L)

((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" ((X `) `)) is M2( the U1 of L)

(X "/\" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" ((X `) `))) is M2( the U1 of L)

((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" ((X "/\" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" ((X `) `)))) is M2( the U1 of L)

(X `) "\/" Y is M2( the U1 of L)

((X `) "\/" Y) "/\" ((Y `) "\/" ((X `) `)) is M2( the U1 of L)

(X "/\" Y) "/\" (((X `) "\/" Y) "/\" ((Y `) "\/" ((X `) `))) is M2( the U1 of L)

((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" ((X "/\" Y) "/\" (((X `) "\/" Y) "/\" ((Y `) "\/" ((X `) `)))) is M2( the U1 of L)

(Y `) "\/" X is M2( the U1 of L)

((X `) "\/" Y) "/\" ((Y `) "\/" X) is M2( the U1 of L)

(X "/\" Y) "/\" (((X `) "\/" Y) "/\" ((Y `) "\/" X)) is M2( the U1 of L)

((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" ((X "/\" Y) "/\" (((X `) "\/" Y) "/\" ((Y `) "\/" X))) is M2( the U1 of L)

(X "/\" Y) "/\" ((X `) "\/" Y) is M2( the U1 of L)

((X "/\" Y) "/\" ((X `) "\/" Y)) "/\" ((Y `) "\/" X) is M2( the U1 of L)

((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" (((X "/\" Y) "/\" ((X `) "\/" Y)) "/\" ((Y `) "\/" X)) is M2( the U1 of L)

(X "/\" Y) "/\" (X `) is M2( the U1 of L)

(X "/\" Y) "/\" Y is M2( the U1 of L)

((X "/\" Y) "/\" (X `)) "\/" ((X "/\" Y) "/\" Y) is M2( the U1 of L)

(((X "/\" Y) "/\" (X `)) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y `) "\/" X) is M2( the U1 of L)

((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" ((((X "/\" Y) "/\" (X `)) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y `) "\/" X)) is M2( the U1 of L)

X "/\" (X `) is M2( the U1 of L)

Y "/\" (X "/\" (X `)) is M2( the U1 of L)

(Y "/\" (X "/\" (X `))) "\/" ((X "/\" Y) "/\" Y) is M2( the U1 of L)

((Y "/\" (X "/\" (X `))) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y `) "\/" X) is M2( the U1 of L)

((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" (((Y "/\" (X "/\" (X `))) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y `) "\/" X)) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

Y "/\" (Bottom L) is M2( the U1 of L)

(Y "/\" (Bottom L)) "\/" ((X "/\" Y) "/\" Y) is M2( the U1 of L)

((Y "/\" (Bottom L)) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y `) "\/" X) is M2( the U1 of L)

((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" (((Y "/\" (Bottom L)) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y `) "\/" X)) is M2( the U1 of L)

Y "/\" Y is M2( the U1 of L)

X "/\" (Y "/\" Y) is M2( the U1 of L)

(X "/\" (Y "/\" Y)) "/\" ((Y `) "\/" X) is M2( the U1 of L)

((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" ((X "/\" (Y "/\" Y)) "/\" ((Y `) "\/" X)) is M2( the U1 of L)

(X "/\" Y) "/\" (Y `) is M2( the U1 of L)

(X "/\" Y) "/\" X is M2( the U1 of L)

((X "/\" Y) "/\" (Y `)) "\/" ((X "/\" Y) "/\" X) is M2( the U1 of L)

((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" (((X "/\" Y) "/\" (Y `)) "\/" ((X "/\" Y) "/\" X)) is M2( the U1 of L)

Y "/\" (Y `) is M2( the U1 of L)

X "/\" (Y "/\" (Y `)) is M2( the U1 of L)

(X "/\" (Y "/\" (Y `))) "\/" ((X "/\" Y) "/\" X) is M2( the U1 of L)

((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" ((X "/\" (Y "/\" (Y `))) "\/" ((X "/\" Y) "/\" X)) is M2( the U1 of L)

X "/\" (Bottom L) is M2( the U1 of L)

(X "/\" (Bottom L)) "\/" ((X "/\" Y) "/\" X) is M2( the U1 of L)

((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" ((X "/\" (Bottom L)) "\/" ((X "/\" Y) "/\" X)) is M2( the U1 of L)

X "/\" X is M2( the U1 of L)

Y "/\" (X "/\" X) is M2( the U1 of L)

((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" (Y "/\" (X "/\" X)) is M2( the U1 of L)

(X "/\" (Y `)) "/\" (X `) is M2( the U1 of L)

(Y "/\" (X `)) "/\" (X `) is M2( the U1 of L)

((X "/\" (Y `)) "/\" (X `)) "\/" ((Y "/\" (X `)) "/\" (X `)) is M2( the U1 of L)

((L,X,Y) "\/" (L,Y,X)) "/\" (Y `) is M2( the U1 of L)

(((X "/\" (Y `)) "/\" (X `)) "\/" ((Y "/\" (X `)) "/\" (X `))) "\/" (((L,X,Y) "\/" (L,Y,X)) "/\" (Y `)) is M2( the U1 of L)

Y "/\" X is M2( the U1 of L)

((((X "/\" (Y `)) "/\" (X `)) "\/" ((Y "/\" (X `)) "/\" (X `))) "\/" (((L,X,Y) "\/" (L,Y,X)) "/\" (Y `))) "\/" (Y "/\" X) is M2( the U1 of L)

(Y `) "/\" (X "/\" (X `)) is M2( the U1 of L)

((Y `) "/\" (X "/\" (X `))) "\/" ((Y "/\" (X `)) "/\" (X `)) is M2( the U1 of L)

(((Y `) "/\" (X "/\" (X `))) "\/" ((Y "/\" (X `)) "/\" (X `))) "\/" (((L,X,Y) "\/" (L,Y,X)) "/\" (Y `)) is M2( the U1 of L)

((((Y `) "/\" (X "/\" (X `))) "\/" ((Y "/\" (X `)) "/\" (X `))) "\/" (((L,X,Y) "\/" (L,Y,X)) "/\" (Y `))) "\/" (Y "/\" X) is M2( the U1 of L)

(X `) "/\" (X `) is M2( the U1 of L)

Y "/\" ((X `) "/\" (X `)) is M2( the U1 of L)

((Y `) "/\" (X "/\" (X `))) "\/" (Y "/\" ((X `) "/\" (X `))) is M2( the U1 of L)

(((Y `) "/\" (X "/\" (X `))) "\/" (Y "/\" ((X `) "/\" (X `)))) "\/" (((L,X,Y) "\/" (L,Y,X)) "/\" (Y `)) is M2( the U1 of L)

((((Y `) "/\" (X "/\" (X `))) "\/" (Y "/\" ((X `) "/\" (X `)))) "\/" (((L,X,Y) "\/" (L,Y,X)) "/\" (Y `))) "\/" (Y "/\" X) is M2( the U1 of L)

(Y `) "/\" (Bottom L) is M2( the U1 of L)

((Y `) "/\" (Bottom L)) "\/" (Y "/\" ((X `) "/\" (X `))) is M2( the U1 of L)

(((Y `) "/\" (Bottom L)) "\/" (Y "/\" ((X `) "/\" (X `)))) "\/" (((L,X,Y) "\/" (L,Y,X)) "/\" (Y `)) is M2( the U1 of L)

((((Y `) "/\" (Bottom L)) "\/" (Y "/\" ((X `) "/\" (X `)))) "\/" (((L,X,Y) "\/" (L,Y,X)) "/\" (Y `))) "\/" (Y "/\" X) is M2( the U1 of L)

(X "/\" (Y `)) "/\" (Y `) is M2( the U1 of L)

(Y "/\" (X `)) "/\" (Y `) is M2( the U1 of L)

((X "/\" (Y `)) "/\" (Y `)) "\/" ((Y "/\" (X `)) "/\" (Y `)) is M2( the U1 of L)

(Y "/\" (X `)) "\/" (((X "/\" (Y `)) "/\" (Y `)) "\/" ((Y "/\" (X `)) "/\" (Y `))) is M2( the U1 of L)

((Y "/\" (X `)) "\/" (((X "/\" (Y `)) "/\" (Y `)) "\/" ((Y "/\" (X `)) "/\" (Y `)))) "\/" (Y "/\" X) is M2( the U1 of L)

(Y `) "/\" (Y `) is M2( the U1 of L)

X "/\" ((Y `) "/\" (Y `)) is M2( the U1 of L)

(X "/\" ((Y `) "/\" (Y `))) "\/" ((Y "/\" (X `)) "/\" (Y `)) is M2( the U1 of L)

(Y "/\" (X `)) "\/" ((X "/\" ((Y `) "/\" (Y `))) "\/" ((Y "/\" (X `)) "/\" (Y `))) is M2( the U1 of L)

((Y "/\" (X `)) "\/" ((X "/\" ((Y `) "/\" (Y `))) "\/" ((Y "/\" (X `)) "/\" (Y `)))) "\/" (Y "/\" X) is M2( the U1 of L)

(X `) "/\" (Y "/\" (Y `)) is M2( the U1 of L)

(X "/\" (Y `)) "\/" ((X `) "/\" (Y "/\" (Y `))) is M2( the U1 of L)

(Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" ((X `) "/\" (Y "/\" (Y `)))) is M2( the U1 of L)

((Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" ((X `) "/\" (Y "/\" (Y `))))) "\/" (Y "/\" X) is M2( the U1 of L)

(X `) "/\" (Bottom L) is M2( the U1 of L)

(X "/\" (Y `)) "\/" ((X `) "/\" (Bottom L)) is M2( the U1 of L)

(Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" ((X `) "/\" (Bottom L))) is M2( the U1 of L)

((Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" ((X `) "/\" (Bottom L)))) "\/" (Y "/\" X) is M2( the U1 of L)

(X "/\" (Y `)) "\/" (Y "/\" X) is M2( the U1 of L)

(Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" (Y "/\" X)) is M2( the U1 of L)

(Y `) "\/" Y is M2( the U1 of L)

X "/\" ((Y `) "\/" Y) is M2( the U1 of L)

(Y "/\" (X `)) "\/" (X "/\" ((Y `) "\/" Y)) is M2( the U1 of L)

Top L is M2( the U1 of L)

X "/\" (Top L) is M2( the U1 of L)

(Y "/\" (X `)) "\/" (X "/\" (Top L)) is M2( the U1 of L)

Y "\/" X is M2( the U1 of L)

(X `) "\/" X is M2( the U1 of L)

(Y "\/" X) "/\" ((X `) "\/" X) is M2( the U1 of L)

(Y "\/" X) "/\" (Top L) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

(L,Y,X) is M2( the U1 of L)

X ` is M2( the U1 of L)

Y "/\" (X `) is M2( the U1 of L)

(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)

X "\/" Y is M2( the U1 of L)

(L,(L,X,Y),(X "\/" Y)) is M2( the U1 of L)

(L,(L,X,Y),(X "\/" Y)) is M2( the U1 of L)

(X "\/" Y) ` is M2( the U1 of L)

(L,X,Y) "/\" ((X "\/" Y) `) is M2( the U1 of L)

(L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)

(L,X,Y) ` is M2( the U1 of L)

(X "\/" Y) "/\" ((L,X,Y) `) is M2( the U1 of L)

(L,(L,X,Y),(X "\/" Y)) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(X `) "/\" (Y `) is M2( the U1 of L)

(L,X,Y) "/\" ((X `) "/\" (Y `)) is M2( the U1 of L)

((L,X,Y) "/\" ((X `) "/\" (Y `))) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)

(X "/\" (Y `)) "/\" ((X `) "/\" (Y `)) is M2( the U1 of L)

(Y "/\" (X `)) "/\" ((X `) "/\" (Y `)) is M2( the U1 of L)

((X "/\" (Y `)) "/\" ((X `) "/\" (Y `))) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `))) is M2( the U1 of L)

(((X "/\" (Y `)) "/\" ((X `) "/\" (Y `))) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `)))) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)

(Y `) "/\" (X `) is M2( the U1 of L)

(Y `) "/\" ((Y `) "/\" (X `)) is M2( the U1 of L)

X "/\" ((Y `) "/\" ((Y `) "/\" (X `))) is M2( the U1 of L)

(X "/\" ((Y `) "/\" ((Y `) "/\" (X `)))) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `))) is M2( the U1 of L)

((X "/\" ((Y `) "/\" ((Y `) "/\" (X `)))) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `)))) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)

(Y `) "/\" (Y `) is M2( the U1 of L)

((Y `) "/\" (Y `)) "/\" (X `) is M2( the U1 of L)

X "/\" (((Y `) "/\" (Y `)) "/\" (X `)) is M2( the U1 of L)

(X "/\" (((Y `) "/\" (Y `)) "/\" (X `))) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `))) is M2( the U1 of L)

((X "/\" (((Y `) "/\" (Y `)) "/\" (X `))) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `)))) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)

X "/\" (X `) is M2( the U1 of L)

(X "/\" (X `)) "/\" (Y `) is M2( the U1 of L)

((X "/\" (X `)) "/\" (Y `)) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `))) is M2( the U1 of L)

(((X "/\" (X `)) "/\" (Y `)) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `)))) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

(Bottom L) "/\" (Y `) is M2( the U1 of L)

((Bottom L) "/\" (Y `)) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `))) is M2( the U1 of L)

(((Bottom L) "/\" (Y `)) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `)))) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)

(X `) "/\" ((X `) "/\" (Y `)) is M2( the U1 of L)

Y "/\" ((X `) "/\" ((X `) "/\" (Y `))) is M2( the U1 of L)

(Y "/\" ((X `) "/\" ((X `) "/\" (Y `)))) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)

(X `) "/\" (X `) is M2( the U1 of L)

((X `) "/\" (X `)) "/\" (Y `) is M2( the U1 of L)

Y "/\" (((X `) "/\" (X `)) "/\" (Y `)) is M2( the U1 of L)

(Y "/\" (((X `) "/\" (X `)) "/\" (Y `))) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)

Y "/\" (Y `) is M2( the U1 of L)

(Y "/\" (Y `)) "/\" (X `) is M2( the U1 of L)

((Y "/\" (Y `)) "/\" (X `)) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)

(Bottom L) "/\" (X `) is M2( the U1 of L)

((Bottom L) "/\" (X `)) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)

Y "/\" X is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

(L,X,Y) is M2( the U1 of L)

Y ` is M2( the U1 of L)

X "/\" (Y `) is M2( the U1 of L)

(L,Y,X) is M2( the U1 of L)

X ` is M2( the U1 of L)

Y "/\" (X `) is M2( the U1 of L)

(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)

X "\/" Y is M2( the U1 of L)

X "/\" Y is M2( the U1 of L)

(L,(X "\/" Y),(X "/\" Y)) is M2( the U1 of L)

(X "/\" Y) ` is M2( the U1 of L)

(X "\/" Y) "/\" ((X "/\" Y) `) is M2( the U1 of L)

(L,X,(X "/\" Y)) is M2( the U1 of L)

X "/\" ((X "/\" Y) `) is M2( the U1 of L)

(L,X,(X "/\" Y)) "\/" (L,Y,X) is M2( the U1 of L)

(L,Y,(X "/\" Y)) is M2( the U1 of L)

Y "/\" ((X "/\" Y) `) is M2( the U1 of L)

(L,X,(X "/\" Y)) "\/" (L,Y,(X "/\" Y)) is M2( the U1 of L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean LattStr

the U1 of L is set

X is M2( the U1 of L)

Y is M2( the U1 of L)

(L,X,Y) is M2( the U1 of