:: 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 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)
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)
X "\/" Z is M2( the U1 of L)
(L,Y,(X "\/" Z)) is M2( the U1 of L)
(X "\/" Z) ` is M2( the U1 of L)
Y "/\" ((X "\/" Z) `) is M2( the U1 of L)
(L,X,(Y "\/" Z)) "\/" (L,Y,(X "\/" Z)) is M2( the U1 of L)
(L,(L,X,Y),Z) is M2( the U1 of L)
(L,X,Y) "/\" (Z `) is M2( the U1 of L)
(L,(L,Y,X),Z) is M2( the U1 of L)
(L,Y,X) "/\" (Z `) is M2( the U1 of L)
(L,(L,X,Y),Z) "\/" (L,(L,Y,X),Z) is M2( the U1 of L)
(L,X,(Y "\/" Z)) "\/" (L,(L,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)
X "/\" Y is M2( the U1 of L)
Z is M2( the U1 of L)
(L,Y,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,Z,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
Z "/\" (Y `) is M2( the U1 of L)
(L,Y,Z) "\/" (L,Z,Y) 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)
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)
(X "/\" Y) "/\" Z is M2( the U1 of L)
(L,X,(Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z) is M2( the U1 of L)
Y "/\" Z is M2( the U1 of L)
(L,(Y "\/" Z),(Y "/\" Z)) is M2( the U1 of L)
(Y "/\" Z) ` is M2( the U1 of L)
(Y "\/" Z) "/\" ((Y "/\" Z) `) is M2( the U1 of L)
(L,X,(L,(Y "\/" Z),(Y "/\" Z))) is M2( the U1 of L)
(L,(Y "\/" Z),(Y "/\" Z)) ` is M2( the U1 of L)
X "/\" ((L,(Y "\/" Z),(Y "/\" Z)) `) is M2( the U1 of L)
X "/\" (Y "/\" Z) is M2( the U1 of L)
(L,X,(Y "\/" Z)) "\/" (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)
(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)
Z is M2( the U1 of L)
(L,(L,X,Y),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)
(L,Z,(L,X,Y)) is M2( the U1 of L)
(L,X,Y) ` is M2( the U1 of L)
Z "/\" ((L,X,Y) `) is M2( the U1 of L)
(L,(L,X,Y),Z) "\/" (L,Z,(L,X,Y)) is M2( the U1 of L)
(L,Y,Z) is M2( the U1 of L)
(L,Y,Z) is M2( the U1 of L)
Y "/\" (Z `) is M2( the U1 of L)
(L,Z,Y) is M2( the U1 of L)
Z "/\" (Y `) is M2( the U1 of L)
(L,Y,Z) "\/" (L,Z,Y) is M2( the U1 of L)
(L,X,(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)
(L,(L,Y,Z),X) is M2( the U1 of L)
(L,Y,Z) "/\" (X `) is M2( the U1 of L)
(L,X,(L,Y,Z)) "\/" (L,(L,Y,Z),X) 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)
X "\/" Z is M2( the U1 of L)
(L,Y,(X "\/" Z)) is M2( the U1 of L)
(X "\/" Z) ` is M2( the U1 of L)
Y "/\" ((X "\/" Z) `) is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)
(L,Z,(X "\/" Y)) is M2( the U1 of L)
(X "\/" Y) ` is M2( the U1 of L)
Z "/\" ((X "\/" 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,(L,X,Y),Z) is M2( the U1 of L)
(L,X,Y) "/\" (Z `) is M2( the U1 of L)
(L,(L,Y,X),Z) is M2( the U1 of L)
(L,Y,X) "/\" (Z `) is M2( the U1 of L)
(L,(L,X,Y),Z) "\/" (L,(L,Y,X),Z) is M2( the U1 of L)
(L,Z,((L,X,Y) "\/" (L,Y,X))) is M2( the U1 of L)
((L,X,Y) "\/" (L,Y,X)) ` is M2( the U1 of L)
Z "/\" (((L,X,Y) "\/" (L,Y,X)) `) is M2( the U1 of L)
((L,(L,X,Y),Z) "\/" (L,(L,Y,X),Z)) "\/" (L,Z,((L,X,Y) "\/" (L,Y,X))) is M2( the U1 of L)
(L,X,(Y "\/" Z)) "\/" (L,(L,Y,X),Z) is M2( the U1 of L)
((L,X,(Y "\/" Z)) "\/" (L,(L,Y,X),Z)) "\/" (L,Z,((L,X,Y) "\/" (L,Y,X))) is M2( the U1 of L)
(L,X,(Y "\/" Z)) "\/" (L,Y,(X "\/" Z)) is M2( the U1 of L)
((L,X,(Y "\/" Z)) "\/" (L,Y,(X "\/" Z))) "\/" (L,Z,((L,X,Y) "\/" (L,Y,X))) 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,Z,(L,(X "\/" Y),(X "/\" Y))) is M2( the U1 of L)
(L,(X "\/" Y),(X "/\" Y)) ` is M2( the U1 of L)
Z "/\" ((L,(X "\/" Y),(X "/\" Y)) `) is M2( the U1 of L)
((L,X,(Y "\/" Z)) "\/" (L,Y,(X "\/" Z))) "\/" (L,Z,(L,(X "\/" Y),(X "/\" Y))) is M2( the U1 of L)
(L,Z,(X "\/" Y)) "\/" ((X "/\" Y) "/\" Z) is M2( the U1 of L)
((L,X,(Y "\/" Z)) "\/" (L,Y,(X "\/" Z))) "\/" ((L,Z,(X "\/" Y)) "\/" ((X "/\" Y) "/\" Z)) is M2( the U1 of L)
((L,X,(Y "\/" Z)) "\/" (L,Y,(X "\/" Z))) "\/" ((X "/\" Y) "/\" Z) is M2( the U1 of L)
(((L,X,(Y "\/" Z)) "\/" (L,Y,(X "\/" Z))) "\/" ((X "/\" Y) "/\" Z)) "\/" (L,Z,(X "\/" Y)) is M2( the U1 of L)
(L,X,(Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z) is M2( the U1 of L)
((L,X,(Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z)) "\/" (L,Y,(X "\/" Z)) is M2( the U1 of L)
(((L,X,(Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z)) "\/" (L,Y,(X "\/" Z))) "\/" (L,Z,(X "\/" Y)) is M2( the U1 of L)
(L,Y,(X "\/" Z)) "\/" (L,Z,(X "\/" Y)) is M2( the U1 of L)
((L,X,(Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z)) "\/" ((L,Y,(X "\/" Z)) "\/" (L,Z,(X "\/" Y))) 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,(Y "\/" Z)) "\/" (X "/\" (Y "/\" Z)) is M2( the U1 of L)
((L,X,(Y "\/" Z)) "\/" (X "/\" (Y "/\" Z))) "\/" ((L,Y,(X "\/" Z)) "\/" (L,Z,(X "\/" Y))) is M2( the U1 of L)
(L,(Y "\/" Z),(Y "/\" Z)) is M2( the U1 of L)
(Y "/\" Z) ` is M2( the U1 of L)
(Y "\/" Z) "/\" ((Y "/\" Z) `) is M2( the U1 of L)
(L,X,(L,(Y "\/" Z),(Y "/\" Z))) is M2( the U1 of L)
(L,(Y "\/" Z),(Y "/\" Z)) ` is M2( the U1 of L)
X "/\" ((L,(Y "\/" Z),(Y "/\" Z)) `) is M2( the U1 of L)
(L,X,(L,(Y "\/" Z),(Y "/\" Z))) "\/" ((L,Y,(X "\/" Z)) "\/" (L,Z,(X "\/" Y))) is M2( the U1 of L)
(L,X,((L,Y,Z) "\/" (L,Z,Y))) is M2( the U1 of L)
((L,Y,Z) "\/" (L,Z,Y)) ` is M2( the U1 of L)
X "/\" (((L,Y,Z) "\/" (L,Z,Y)) `) is M2( the U1 of L)
(L,X,((L,Y,Z) "\/" (L,Z,Y))) "\/" ((L,Y,(X "\/" Z)) "\/" (L,Z,(X "\/" Y))) is M2( the U1 of L)
(L,(L,Z,Y),X) is M2( the U1 of L)
(L,Z,Y) "/\" (X `) is M2( the U1 of L)
(L,Y,(X "\/" Z)) "\/" (L,(L,Z,Y),X) is M2( the U1 of L)
(L,X,((L,Y,Z) "\/" (L,Z,Y))) "\/" ((L,Y,(X "\/" Z)) "\/" (L,(L,Z,Y),X)) is M2( the U1 of L)
(L,(L,Y,Z),X) is M2( the U1 of L)
(L,Y,Z) "/\" (X `) is M2( the U1 of L)
(L,(L,Y,Z),X) "\/" (L,(L,Z,Y),X) is M2( the U1 of L)
(L,X,((L,Y,Z) "\/" (L,Z,Y))) "\/" ((L,(L,Y,Z),X) "\/" (L,(L,Z,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)
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)
Y "/\" (X `) is M2( the U1 of L)
(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)
(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)
(X "/\" Y) "\/" ((X `) "/\" (Y `)) is M2( the U1 of L)
(L,X,Y) ` is M2( the U1 of L)
(L,Y,X) ` is M2( the U1 of L)
((L,X,Y) `) "/\" ((L,Y,X) `) is M2( the U1 of L)
(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 `) ` 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 is M2( the U1 of L)
((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) is M2( the U1 of L)
Y "/\" ((Y `) "\/" X) 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 `) "/\" (Y `)) "\/" ((X `) "/\" X) is M2( the U1 of L)
(((X `) "/\" (Y `)) "\/" ((X `) "/\" X)) "\/" (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)
(((X `) "/\" (Y `)) "\/" ((X `) "/\" X)) "\/" ((Y "/\" (Y `)) "\/" (Y "/\" X)) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
((X `) "/\" (Y `)) "\/" (Bottom L) is M2( the U1 of L)
(((X `) "/\" (Y `)) "\/" (Bottom L)) "\/" ((Y "/\" (Y `)) "\/" (Y "/\" X)) is M2( the U1 of L)
(Bottom L) "\/" (Y "/\" X) is M2( the U1 of L)
((X `) "/\" (Y `)) "\/" ((Bottom L) "\/" (Y "/\" X)) is M2( the U1 of L)