:: ROBBINS2 semantic presentation

K87() is set
K19(K87()) is set
1 is set
K14() is set
TrivComplLat is non empty V42() V43() V48(1) join-commutative join-associative upper-bounded strict Robbins Huntington join-idempotent with_idempotent_element ComplLLattStr
the U1 of TrivComplLat is V11() V12() V28() set
c₁ is M2( the U1 of TrivComplLat)
L9 is M2( the U1 of TrivComplLat)
c₁ + L9 is M2( the U1 of TrivComplLat)
(c₁ + L9) ` is M2( the U1 of TrivComplLat)
x is M2( the U1 of TrivComplLat)
((c<sub>1</sub> + L9) `) + x is M2( the U1 of TrivComplLat)
(((c₁ + L9) `) + x) ` is M2( the U1 of TrivComplLat)
x ` is M2( the U1 of TrivComplLat)
y is M2( the U1 of TrivComplLat)
x + y is M2( the U1 of TrivComplLat)
(x + y) ` is M2( the U1 of TrivComplLat)
(x `) + ((x + y) `) is M2( the U1 of TrivComplLat)
((x `) + ((x + y) `)) ` is M2( the U1 of TrivComplLat)
c<sub>1</sub> + (((x `) + ((x + y) `)) `) is M2( the U1 of TrivComplLat)
(c₁ + (((x `) + ((x + y) `)) `)) ` is M2( the U1 of TrivComplLat)
((((c₁ + L9) `) + x) `) + ((c₁ + (((x `) + ((x + y) `)) `)) `) is M2( the U1 of TrivComplLat)
(((((c₁ + L9) `) + x) `) + ((c₁ + (((x `) + ((x + y) `)) `)) `)) ` is M2( the U1 of TrivComplLat)
TrivOrtLat is non empty V42() V43() V48(1) join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean strict Robbins Huntington join-idempotent well-complemented de_Morgan OrthoLattStr
the U1 of TrivOrtLat is V11() V12() V28() set
c<sub>1</sub> is M2( the U1 of TrivOrtLat)
L9 is M2( the U1 of TrivOrtLat)
c<sub>1</sub> + L9 is M2( the U1 of TrivOrtLat)
(c<sub>1</sub> + L9) ` is M2( the U1 of TrivOrtLat)
x is M2( the U1 of TrivOrtLat)
((c₁ + L9) `) + x is M2( the U1 of TrivOrtLat)
(((c<sub>1</sub> + L9) `) + x) ` is M2( the U1 of TrivOrtLat)
x ` is M2( the U1 of TrivOrtLat)
y is M2( the U1 of TrivOrtLat)
x + y is M2( the U1 of TrivOrtLat)
(x + y) ` is M2( the U1 of TrivOrtLat)
(x `) + ((x + y) `) is M2( the U1 of TrivOrtLat)
((x `) + ((x + y) `)) ` is M2( the U1 of TrivOrtLat)
c₁ + (((x `) + ((x + y) `)) `) is M2( the U1 of TrivOrtLat)
(c<sub>1</sub> + (((x `) + ((x + y) `)) `)) ` is M2( the U1 of TrivOrtLat)
((((c<sub>1</sub> + L9) `) + x) `) + ((c<sub>1</sub> + (((x `) + ((x + y) `)) `)) `) is M2( the U1 of TrivOrtLat)
(((((c<sub>1</sub> + L9) `) + x) `) + ((c<sub>1</sub> + (((x `) + ((x + y) `)) `)) `)) ` is M2( the U1 of TrivOrtLat)
c₁ is non empty () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
L9 + x is M2( the U1 of c₁)
(L9 + x) ` is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
z is M2( the U1 of c<sub>1</sub>)
y + z is M2( the U1 of c<sub>1</sub>)
(y + z) ` is M2( the U1 of c₁)
((y + z) `) + L9 is M2( the U1 of c<sub>1</sub>)
(((y + z) `) + L9) ` is M2( the U1 of c<sub>1</sub>)
x ` is M2( the U1 of c₁)
Z is M2( the U1 of c₁)
x + Z is M2( the U1 of c₁)
(x + Z) ` is M2( the U1 of c<sub>1</sub>)
(x `) + ((x + Z) `) is M2( the U1 of c<sub>1</sub>)
((x `) + ((x + Z) `)) ` is M2( the U1 of c₁)
((((y + z) `) + L9) `) + (((x `) + ((x + Z) `)) `) is M2( the U1 of c<sub>1</sub>)
(((((y + z) `) + L9) `) + (((x `) + ((x + Z) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) + ((((((y + z) `) + L9) `) + (((x `) + ((x + Z) `)) `)) `) is M2( the U1 of c₁)
(((L9 + x) `) + ((((((y + z) `) + L9) `) + (((x `) + ((x + Z) `)) `)) `)) ` is M2( the U1 of c₁)
L9 ` is M2( the U1 of c<sub>1</sub>)
L9 + z is M2( the U1 of c<sub>1</sub>)
(L9 + z) ` is M2( the U1 of c₁)
(L9 `) + ((L9 + z) `) is M2( the U1 of c₁)
((L9 `) + ((L9 + z) `)) ` is M2( the U1 of c<sub>1</sub>)
y + (((L9 `) + ((L9 + z) `)) `) is M2( the U1 of c₁)
(y + (((L9 `) + ((L9 + z) `)) `)) ` is M2( the U1 of c₁)
((((y + z) `) + L9) `) + ((y + (((L9 `) + ((L9 + z) `)) `)) `) is M2( the U1 of c₁)
(((((y + z) `) + L9) `) + ((y + (((L9 `) + ((L9 + z) `)) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
((((((y + z) `) + L9) `) + ((y + (((L9 `) + ((L9 + z) `)) `)) `)) `) + x is M2( the U1 of c₁)
(((((((y + z) `) + L9) `) + ((y + (((L9 `) + ((L9 + z) `)) `)) `)) `) + x) ` is M2( the U1 of c₁)
((((((((y + z) `) + L9) `) + ((y + (((L9 `) + ((L9 + z) `)) `)) `)) `) + x) `) + ((((((y + z) `) + L9) `) + (((x `) + ((x + Z) `)) `)) `) is M2( the U1 of c₁)
(((((((((y + z) `) + L9) `) + ((y + (((L9 `) + ((L9 + z) `)) `)) `)) `) + x) `) + ((((((y + z) `) + L9) `) + (((x `) + ((x + Z) `)) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
y is M2( the U1 of c₁)
y + L9 is M2( the U1 of c₁)
(y + L9) ` is M2( the U1 of c<sub>1</sub>)
x ` is M2( the U1 of c₁)
z is M2( the U1 of c₁)
x + z is M2( the U1 of c₁)
(x + z) ` is M2( the U1 of c<sub>1</sub>)
(x `) + ((x + z) `) is M2( the U1 of c<sub>1</sub>)
((x `) + ((x + z) `)) ` is M2( the U1 of c₁)
((y + L9) `) + (((x `) + ((x + z) `)) `) is M2( the U1 of c₁)
(((y + L9) `) + (((x `) + ((x + z) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) + ((((y + L9) `) + (((x `) + ((x + z) `)) `)) `) is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + ((((y + L9) `) + (((x `) + ((x + z) `)) `)) `)) ` is M2( the U1 of c₁)
the M2( the U1 of c₁) is M2( the U1 of c₁)
L9 + y is M2( the U1 of c₁)
(L9 + y) ` is M2( the U1 of c<sub>1</sub>)
((x + z) `) + L9 is M2( the U1 of c₁)
(((x + z) `) + L9) ` is M2( the U1 of c₁)
y ` is M2( the U1 of c<sub>1</sub>)
y + the M2( the U1 of c<sub>1</sub>) is M2( the U1 of c<sub>1</sub>)
(y + the M2( the U1 of c<sub>1</sub>)) ` is M2( the U1 of c₁)
(y `) + ((y + the M2( the U1 of c<sub>1</sub>)) `) is M2( the U1 of c₁)
((y `) + ((y + the M2( the U1 of c<sub>1</sub>)) `)) ` is M2( the U1 of c<sub>1</sub>)
((((x + z) `) + L9) `) + (((y `) + ((y + the M2( the U1 of c₁)) `)) `) is M2( the U1 of c₁)
(((((x + z) `) + L9) `) + (((y `) + ((y + the M2( the U1 of c<sub>1</sub>)) `)) `)) ` is M2( the U1 of c₁)
((L9 + y) `) + ((((((x + z) `) + L9) `) + (((y `) + ((y + the M2( the U1 of c₁)) `)) `)) `) is M2( the U1 of c<sub>1</sub>)
(((L9 + y) `) + ((((((x + z) `) + L9) `) + (((y `) + ((y + the M2( the U1 of c<sub>1</sub>)) `)) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
L9 + (L9 `) is M2( the U1 of c<sub>1</sub>)
(L9 + (L9 `)) ` is M2( the U1 of c<sub>1</sub>)
((L9 + (L9 `)) `) + L9 is M2( the U1 of c<sub>1</sub>)
(((L9 + (L9 `)) `) + L9) ` is M2( the U1 of c₁)
the M2( the U1 of c₁) is M2( the U1 of c₁)
L9 + the M2( the U1 of c₁) is M2( the U1 of c₁)
(L9 + the M2( the U1 of c₁)) ` is M2( the U1 of c<sub>1</sub>)
(L9 `) ` is M2( the U1 of c<sub>1</sub>)
((L9 `) `) + the M2( the U1 of c<sub>1</sub>) is M2( the U1 of c<sub>1</sub>)
(((L9 `) `) + the M2( the U1 of c<sub>1</sub>)) ` is M2( the U1 of c₁)
((((L9 `) `) + the M2( the U1 of c₁)) `) + L9 is M2( the U1 of c<sub>1</sub>)
(((((L9 `) `) + the M2( the U1 of c<sub>1</sub>)) `) + L9) ` is M2( the U1 of c<sub>1</sub>)
(L9 `) + ((L9 + the M2( the U1 of c₁)) `) is M2( the U1 of c<sub>1</sub>)
((L9 `) + ((L9 + the M2( the U1 of c₁)) `)) ` is M2( the U1 of c₁)
((L9 `) `) + (((L9 `) + ((L9 + the M2( the U1 of c<sub>1</sub>)) `)) `) is M2( the U1 of c<sub>1</sub>)
(((L9 `) `) + (((L9 `) + ((L9 + the M2( the U1 of c₁)) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
((((((L9 `) `) + the M2( the U1 of c<sub>1</sub>)) `) + L9) `) + ((((L9 `) `) + (((L9 `) + ((L9 + the M2( the U1 of c₁)) `)) `)) `) is M2( the U1 of c<sub>1</sub>)
(((((((L9 `) `) + the M2( the U1 of c<sub>1</sub>)) `) + L9) `) + ((((L9 `) `) + (((L9 `) + ((L9 + the M2( the U1 of c₁)) `)) `)) `)) ` is M2( the U1 of c₁)
((L9 + (L9 `)) `) + ((((((((L9 `) `) + the M2( the U1 of c₁)) `) + L9) `) + ((((L9 `) `) + (((L9 `) + ((L9 + the M2( the U1 of c<sub>1</sub>)) `)) `)) `)) `) is M2( the U1 of c<sub>1</sub>)
(((L9 + (L9 `)) `) + ((((((((L9 `) `) + the M2( the U1 of c<sub>1</sub>)) `) + L9) `) + ((((L9 `) `) + (((L9 `) + ((L9 + the M2( the U1 of c₁)) `)) `)) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
y is M2( the U1 of c₁)
y + L9 is M2( the U1 of c₁)
(y + L9) ` is M2( the U1 of c<sub>1</sub>)
x ` is M2( the U1 of c₁)
x + (x `) is M2( the U1 of c<sub>1</sub>)
(x + (x `)) ` is M2( the U1 of c<sub>1</sub>)
((x + (x `)) `) + x is M2( the U1 of c<sub>1</sub>)
(((x + (x `)) `) + x) ` is M2( the U1 of c₁)
z is M2( the U1 of c₁)
x + z is M2( the U1 of c₁)
(x + z) ` is M2( the U1 of c<sub>1</sub>)
((((x + (x `)) `) + x) `) + ((x + z) `) is M2( the U1 of c<sub>1</sub>)
(((((x + (x `)) `) + x) `) + ((x + z) `)) ` is M2( the U1 of c₁)
((y + L9) `) + ((((((x + (x `)) `) + x) `) + ((x + z) `)) `) is M2( the U1 of c₁)
(((y + L9) `) + ((((((x + (x `)) `) + x) `) + ((x + z) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) + ((((y + L9) `) + ((((((x + (x `)) `) + x) `) + ((x + z) `)) `)) `) is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + ((((y + L9) `) + ((((((x + (x `)) `) + x) `) + ((x + z) `)) `)) `)) ` is M2( the U1 of c₁)
c₁ is non empty () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
L9 + x is M2( the U1 of c₁)
(L9 + x) ` is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
y + L9 is M2( the U1 of c<sub>1</sub>)
(y + L9) ` is M2( the U1 of c₁)
((y + L9) `) + x is M2( the U1 of c<sub>1</sub>)
(((y + L9) `) + x) ` is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) + ((((y + L9) `) + x) `) is M2( the U1 of c₁)
(((L9 + x) `) + ((((y + L9) `) + x) `)) ` is M2( the U1 of c₁)
the M2( the U1 of c₁) is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
x + the M2( the U1 of c<sub>1</sub>) is M2( the U1 of c<sub>1</sub>)
(x + the M2( the U1 of c<sub>1</sub>)) ` is M2( the U1 of c₁)
(x `) + ((x + the M2( the U1 of c<sub>1</sub>)) `) is M2( the U1 of c₁)
((x `) + ((x + the M2( the U1 of c<sub>1</sub>)) `)) ` is M2( the U1 of c<sub>1</sub>)
x + (x `) is M2( the U1 of c₁)
(x + (x `)) ` is M2( the U1 of c₁)
((x + (x `)) `) + x is M2( the U1 of c₁)
(((x + (x `)) `) + x) ` is M2( the U1 of c<sub>1</sub>)
x + (((x `) + ((x + the M2( the U1 of c₁)) `)) `) is M2( the U1 of c₁)
(x + (((x `) + ((x + the M2( the U1 of c<sub>1</sub>)) `)) `)) ` is M2( the U1 of c₁)
((((x + (x `)) `) + x) `) + ((x + (((x `) + ((x + the M2( the U1 of c₁)) `)) `)) `) is M2( the U1 of c<sub>1</sub>)
(((((x + (x `)) `) + x) `) + ((x + (((x `) + ((x + the M2( the U1 of c<sub>1</sub>)) `)) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
((y + L9) `) + ((((((x + (x `)) `) + x) `) + ((x + (((x `) + ((x + the M2( the U1 of c₁)) `)) `)) `)) `) is M2( the U1 of c₁)
(((y + L9) `) + ((((((x + (x `)) `) + x) `) + ((x + (((x `) + ((x + the M2( the U1 of c<sub>1</sub>)) `)) `)) `)) `)) ` is M2( the U1 of c₁)
((L9 + x) `) + ((((y + L9) `) + ((((((x + (x `)) `) + x) `) + ((x + (((x `) + ((x + the M2( the U1 of c₁)) `)) `)) `)) `)) `) is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + ((((y + L9) `) + ((((((x + (x `)) `) + x) `) + ((x + (((x `) + ((x + the M2( the U1 of c<sub>1</sub>)) `)) `)) `)) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
L9 ` is M2( the U1 of c<sub>1</sub>)
(L9 `) + x is M2( the U1 of c₁)
((L9 `) + x) ` is M2( the U1 of c₁)
((L9 + x) `) + (((L9 `) + x) `) is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + (((L9 `) + x) `)) ` is M2( the U1 of c<sub>1</sub>)
L9 + (L9 `) is M2( the U1 of c₁)
(L9 + (L9 `)) ` is M2( the U1 of c₁)
((L9 + (L9 `)) `) + L9 is M2( the U1 of c₁)
(((L9 + (L9 `)) `) + L9) ` is M2( the U1 of c<sub>1</sub>)
((((L9 + (L9 `)) `) + L9) `) + x is M2( the U1 of c₁)
(((((L9 + (L9 `)) `) + L9) `) + x) ` is M2( the U1 of c₁)
((L9 + x) `) + ((((((L9 + (L9 `)) `) + L9) `) + x) `) is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + ((((((L9 + (L9 `)) `) + L9) `) + x) `)) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
((L9 + x) `) + L9 is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + L9) ` is M2( the U1 of c<sub>1</sub>)
((((L9 + x) `) + L9) `) + ((L9 + x) `) is M2( the U1 of c₁)
(((((L9 + x) `) + L9) `) + ((L9 + x) `)) ` is M2( the U1 of c₁)
L9 + ((L9 + x) `) is M2( the U1 of c<sub>1</sub>)
(L9 + ((L9 + x) `)) ` is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
L9 + (L9 `) is M2( the U1 of c<sub>1</sub>)
(L9 + (L9 `)) ` is M2( the U1 of c<sub>1</sub>)
((L9 + (L9 `)) `) + L9 is M2( the U1 of c<sub>1</sub>)
(((L9 + (L9 `)) `) + L9) ` is M2( the U1 of c₁)
((((L9 + (L9 `)) `) + L9) `) + ((L9 + x) `) is M2( the U1 of c₁)
(((((L9 + (L9 `)) `) + L9) `) + ((L9 + x) `)) ` is M2( the U1 of c<sub>1</sub>)
((L9 + ((L9 + x) `)) `) + ((((((L9 + (L9 `)) `) + L9) `) + ((L9 + x) `)) `) is M2( the U1 of c₁)
(((L9 + ((L9 + x) `)) `) + ((((((L9 + (L9 `)) `) + L9) `) + ((L9 + x) `)) `)) ` is M2( the U1 of c₁)
((((L9 + x) `) + L9) `) + ((((L9 + ((L9 + x) `)) `) + ((((((L9 + (L9 `)) `) + L9) `) + ((L9 + x) `)) `)) `) is M2( the U1 of c₁)
(((((L9 + x) `) + L9) `) + ((((L9 + ((L9 + x) `)) `) + ((((((L9 + (L9 `)) `) + L9) `) + ((L9 + x) `)) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
((L9 + x) `) + L9 is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + L9) ` is M2( the U1 of c<sub>1</sub>)
L9 + ((((L9 + x) `) + L9) `) is M2( the U1 of c<sub>1</sub>)
(L9 + ((((L9 + x) `) + L9) `)) ` is M2( the U1 of c₁)
((((L9 + x) `) + L9) `) + ((L9 + x) `) is M2( the U1 of c<sub>1</sub>)
(((((L9 + x) `) + L9) `) + ((L9 + x) `)) ` is M2( the U1 of c<sub>1</sub>)
((((((L9 + x) `) + L9) `) + ((L9 + x) `)) `) + ((((L9 + x) `) + L9) `) is M2( the U1 of c<sub>1</sub>)
(((((((L9 + x) `) + L9) `) + ((L9 + x) `)) `) + ((((L9 + x) `) + L9) `)) ` is M2( the U1 of c₁)
c₁ is non empty () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
L9 + x is M2( the U1 of c₁)
(L9 + x) ` is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) + y is M2( the U1 of c₁)
(((L9 + x) `) + y) ` is M2( the U1 of c₁)
L9 + y is M2( the U1 of c₁)
(L9 + y) ` is M2( the U1 of c<sub>1</sub>)
((((L9 + x) `) + y) `) + ((L9 + y) `) is M2( the U1 of c₁)
(((((L9 + x) `) + y) `) + ((L9 + y) `)) ` is M2( the U1 of c₁)
((L9 + x) `) + L9 is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + L9) ` is M2( the U1 of c<sub>1</sub>)
((((L9 + x) `) + L9) `) + ((L9 + x) `) is M2( the U1 of c₁)
(((((L9 + x) `) + L9) `) + ((L9 + x) `)) ` is M2( the U1 of c₁)
((((((L9 + x) `) + L9) `) + ((L9 + x) `)) `) + y is M2( the U1 of c₁)
(((((((L9 + x) `) + L9) `) + ((L9 + x) `)) `) + y) ` is M2( the U1 of c<sub>1</sub>)
((((L9 + x) `) + y) `) + ((((((((L9 + x) `) + L9) `) + ((L9 + x) `)) `) + y) `) is M2( the U1 of c₁)
(((((L9 + x) `) + y) `) + ((((((((L9 + x) `) + L9) `) + ((L9 + x) `)) `) + y) `)) ` is M2( the U1 of c₁)
c₁ is non empty () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
y is M2( the U1 of c₁)
x + y is M2( the U1 of c₁)
(x + y) ` is M2( the U1 of c<sub>1</sub>)
x + L9 is M2( the U1 of c<sub>1</sub>)
(x + L9) ` is M2( the U1 of c₁)
((x + y) `) + ((x + L9) `) is M2( the U1 of c₁)
(((x + y) `) + ((x + L9) `)) ` is M2( the U1 of c<sub>1</sub>)
L9 + ((((x + y) `) + ((x + L9) `)) `) is M2( the U1 of c₁)
(L9 + ((((x + y) `) + ((x + L9) `)) `)) ` is M2( the U1 of c₁)
((x + y) `) + L9 is M2( the U1 of c<sub>1</sub>)
(((x + y) `) + L9) ` is M2( the U1 of c<sub>1</sub>)
((((x + y) `) + L9) `) + ((x + L9) `) is M2( the U1 of c₁)
(((((x + y) `) + L9) `) + ((x + L9) `)) ` is M2( the U1 of c₁)
((((((x + y) `) + L9) `) + ((x + L9) `)) `) + ((((x + y) `) + ((x + L9) `)) `) is M2( the U1 of c<sub>1</sub>)
(((((((x + y) `) + L9) `) + ((x + L9) `)) `) + ((((x + y) `) + ((x + L9) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
y is M2( the U1 of c₁)
((L9 + x) `) + y is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + y) ` is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
(L9 `) + x is M2( the U1 of c<sub>1</sub>)
((L9 `) + x) ` is M2( the U1 of c<sub>1</sub>)
((((L9 + x) `) + y) `) + (((L9 `) + x) `) is M2( the U1 of c<sub>1</sub>)
(((((L9 + x) `) + y) `) + (((L9 `) + x) `)) ` is M2( the U1 of c₁)
((((((L9 + x) `) + y) `) + (((L9 `) + x) `)) `) + x is M2( the U1 of c<sub>1</sub>)
(((((((L9 + x) `) + y) `) + (((L9 `) + x) `)) `) + x) ` is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) + (((L9 `) + x) `) is M2( the U1 of c₁)
(((L9 + x) `) + (((L9 `) + x) `)) ` is M2( the U1 of c₁)
((((((L9 + x) `) + y) `) + (((L9 `) + x) `)) `) + ((((L9 + x) `) + (((L9 `) + x) `)) `) is M2( the U1 of c<sub>1</sub>)
(((((((L9 + x) `) + y) `) + (((L9 `) + x) `)) `) + ((((L9 + x) `) + (((L9 `) + x) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
x + y is M2( the U1 of c<sub>1</sub>)
(x + y) ` is M2( the U1 of c₁)
y + L9 is M2( the U1 of c₁)
(y + L9) ` is M2( the U1 of c<sub>1</sub>)
((x + y) `) + ((y + L9) `) is M2( the U1 of c<sub>1</sub>)
(((x + y) `) + ((y + L9) `)) ` is M2( the U1 of c₁)
L9 + ((((x + y) `) + ((y + L9) `)) `) is M2( the U1 of c<sub>1</sub>)
(L9 + ((((x + y) `) + ((y + L9) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
x + L9 is M2( the U1 of c<sub>1</sub>)
(x + L9) ` is M2( the U1 of c₁)
((x + L9) `) + ((x + y) `) is M2( the U1 of c₁)
(((x + L9) `) + ((x + y) `)) ` is M2( the U1 of c<sub>1</sub>)
y + ((((x + L9) `) + ((x + y) `)) `) is M2( the U1 of c₁)
(y + ((((x + L9) `) + ((x + y) `)) `)) ` is M2( the U1 of c₁)
((y + ((((x + L9) `) + ((x + y) `)) `)) `) + ((y + L9) `) is M2( the U1 of c<sub>1</sub>)
(((y + ((((x + L9) `) + ((x + y) `)) `)) `) + ((y + L9) `)) ` is M2( the U1 of c<sub>1</sub>)
L9 + ((((y + ((((x + L9) `) + ((x + y) `)) `)) `) + ((y + L9) `)) `) is M2( the U1 of c<sub>1</sub>)
(L9 + ((((y + ((((x + L9) `) + ((x + y) `)) `)) `) + ((y + L9) `)) `)) ` is M2( the U1 of c₁)
c₁ is non empty () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
L9 + x is M2( the U1 of c₁)
(L9 + x) ` is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
y + L9 is M2( the U1 of c<sub>1</sub>)
(y + L9) ` is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
z is M2( the U1 of c<sub>1</sub>)
z + x is M2( the U1 of c<sub>1</sub>)
(z + x) ` is M2( the U1 of c₁)
(x `) + ((z + x) `) is M2( the U1 of c₁)
((x `) + ((z + x) `)) ` is M2( the U1 of c<sub>1</sub>)
((y + L9) `) + (((x `) + ((z + x) `)) `) is M2( the U1 of c<sub>1</sub>)
(((y + L9) `) + (((x `) + ((z + x) `)) `)) ` is M2( the U1 of c₁)
((L9 + x) `) + ((((y + L9) `) + (((x `) + ((z + x) `)) `)) `) is M2( the U1 of c₁)
(((L9 + x) `) + ((((y + L9) `) + (((x `) + ((z + x) `)) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
z + y is M2( the U1 of c<sub>1</sub>)
(z + y) ` is M2( the U1 of c₁)
((z + y) `) + ((z + x) `) is M2( the U1 of c₁)
(((z + y) `) + ((z + x) `)) ` is M2( the U1 of c<sub>1</sub>)
x + ((((z + y) `) + ((z + x) `)) `) is M2( the U1 of c₁)
(x + ((((z + y) `) + ((z + x) `)) `)) ` is M2( the U1 of c₁)
(x `) + ((x + ((((z + y) `) + ((z + x) `)) `)) `) is M2( the U1 of c<sub>1</sub>)
((x `) + ((x + ((((z + y) `) + ((z + x) `)) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
((y + L9) `) + (((x `) + ((x + ((((z + y) `) + ((z + x) `)) `)) `)) `) is M2( the U1 of c₁)
(((y + L9) `) + (((x `) + ((x + ((((z + y) `) + ((z + x) `)) `)) `)) `)) ` is M2( the U1 of c₁)
((L9 + x) `) + ((((y + L9) `) + (((x `) + ((x + ((((z + y) `) + ((z + x) `)) `)) `)) `)) `) is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + ((((y + L9) `) + (((x `) + ((x + ((((z + y) `) + ((z + x) `)) `)) `)) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
x + L9 is M2( the U1 of c₁)
(x + L9) ` is M2( the U1 of c<sub>1</sub>)
((x + L9) `) + x is M2( the U1 of c₁)
(((x + L9) `) + x) ` is M2( the U1 of c₁)
((((x + L9) `) + x) `) + ((x + L9) `) is M2( the U1 of c<sub>1</sub>)
(((((x + L9) `) + x) `) + ((x + L9) `)) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
y is M2( the U1 of c₁)
x + y is M2( the U1 of c₁)
(x + y) ` is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) + ((x + y) `) is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + ((x + y) `)) ` is M2( the U1 of c₁)
((((L9 + x) `) + ((x + y) `)) `) + y is M2( the U1 of c<sub>1</sub>)
(((((L9 + x) `) + ((x + y) `)) `) + y) ` is M2( the U1 of c<sub>1</sub>)
y + ((((L9 + x) `) + ((x + y) `)) `) is M2( the U1 of c₁)
(y + ((((L9 + x) `) + ((x + y) `)) `)) ` is M2( the U1 of c₁)
c₁ is non empty () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
L9 + x is M2( the U1 of c₁)
(L9 + x) ` is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) + y is M2( the U1 of c₁)
(((L9 + x) `) + y) ` is M2( the U1 of c₁)
L9 + ((((L9 + x) `) + y) `) is M2( the U1 of c₁)
(L9 + ((((L9 + x) `) + y) `)) ` is M2( the U1 of c<sub>1</sub>)
((L9 + ((((L9 + x) `) + y) `)) `) + y is M2( the U1 of c₁)
(((L9 + ((((L9 + x) `) + y) `)) `) + y) ` is M2( the U1 of c₁)
((L9 + x) `) + L9 is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + L9) ` is M2( the U1 of c<sub>1</sub>)
((((L9 + x) `) + L9) `) + ((L9 + x) `) is M2( the U1 of c₁)
(((((L9 + x) `) + L9) `) + ((L9 + x) `)) ` is M2( the U1 of c₁)
c₁ is non empty () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
L9 + x is M2( the U1 of c₁)
(L9 + x) ` is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) + L9 is M2( the U1 of c₁)
(((L9 + x) `) + L9) ` is M2( the U1 of c₁)
((((L9 + x) `) + L9) `) + x is M2( the U1 of c₁)
(((((L9 + x) `) + L9) `) + x) ` is M2( the U1 of c<sub>1</sub>)
x + x is M2( the U1 of c<sub>1</sub>)
(x + x) ` is M2( the U1 of c₁)
((L9 + x) `) + ((((((L9 + x) `) + L9) `) + x) `) is M2( the U1 of c₁)
(((L9 + x) `) + ((((((L9 + x) `) + L9) `) + x) `)) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
x is M2( the U1 of c₁)
x + L9 is M2( the U1 of c₁)
(x + L9) ` is M2( the U1 of c<sub>1</sub>)
(L9 `) + ((x + L9) `) is M2( the U1 of c<sub>1</sub>)
((L9 `) + ((x + L9) `)) ` is M2( the U1 of c₁)
(L9 `) + x is M2( the U1 of c<sub>1</sub>)
((L9 `) + x) ` is M2( the U1 of c<sub>1</sub>)
(((L9 `) + x) `) + (((L9 `) + ((x + L9) `)) `) is M2( the U1 of c₁)
((((L9 `) + x) `) + (((L9 `) + ((x + L9) `)) `)) ` is M2( the U1 of c₁)
((x + L9) `) + (((((L9 `) + x) `) + (((L9 `) + ((x + L9) `)) `)) `) is M2( the U1 of c<sub>1</sub>)
(((x + L9) `) + (((((L9 `) + x) `) + (((L9 `) + ((x + L9) `)) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) + (x `) is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + (x `)) ` is M2( the U1 of c₁)
(x `) + ((L9 + x) `) is M2( the U1 of c₁)
((x `) + ((L9 + x) `)) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
x + (L9 `) is M2( the U1 of c<sub>1</sub>)
(x + (L9 `)) ` is M2( the U1 of c<sub>1</sub>)
L9 + ((x + (L9 `)) `) is M2( the U1 of c<sub>1</sub>)
(L9 + ((x + (L9 `)) `)) ` is M2( the U1 of c₁)
x + L9 is M2( the U1 of c₁)
(x + L9) ` is M2( the U1 of c<sub>1</sub>)
((x + L9) `) + (L9 `) is M2( the U1 of c<sub>1</sub>)
(((x + L9) `) + (L9 `)) ` is M2( the U1 of c₁)
((((x + L9) `) + (L9 `)) `) + ((x + (L9 `)) `) is M2( the U1 of c<sub>1</sub>)
(((((x + L9) `) + (L9 `)) `) + ((x + (L9 `)) `)) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
L9 + L9 is M2( the U1 of c<sub>1</sub>)
(L9 + L9) ` is M2( the U1 of c₁)
L9 ` is M2( the U1 of c<sub>1</sub>)
the M2( the U1 of c<sub>1</sub>) is M2( the U1 of c<sub>1</sub>)
the M2( the U1 of c<sub>1</sub>) + L9 is M2( the U1 of c<sub>1</sub>)
( the M2( the U1 of c<sub>1</sub>) + L9) ` is M2( the U1 of c₁)
(( the M2( the U1 of c₁) + L9) `) + (L9 `) is M2( the U1 of c₁)
((( the M2( the U1 of c₁) + L9) `) + (L9 `)) ` is M2( the U1 of c<sub>1</sub>)
L9 + (((( the M2( the U1 of c<sub>1</sub>) + L9) `) + (L9 `)) `) is M2( the U1 of c₁)
(L9 + (((( the M2( the U1 of c₁) + L9) `) + (L9 `)) `)) ` is M2( the U1 of c₁)
c₁ is non empty () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
L9 + x is M2( the U1 of c₁)
(L9 + x) ` is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) + L9 is M2( the U1 of c₁)
(((L9 + x) `) + L9) ` is M2( the U1 of c₁)
((((L9 + x) `) + L9) `) + x is M2( the U1 of c₁)
(((((L9 + x) `) + L9) `) + x) ` is M2( the U1 of c<sub>1</sub>)
x ` is M2( the U1 of c₁)
x + x is M2( the U1 of c₁)
(x + x) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
(L9 `) ` is M2( the U1 of c₁)
L9 + (L9 `) is M2( the U1 of c<sub>1</sub>)
(L9 + (L9 `)) ` is M2( the U1 of c<sub>1</sub>)
((L9 + (L9 `)) `) + L9 is M2( the U1 of c<sub>1</sub>)
(((L9 + (L9 `)) `) + L9) ` is M2( the U1 of c₁)
((((L9 + (L9 `)) `) + L9) `) + (L9 `) is M2( the U1 of c₁)
(((((L9 + (L9 `)) `) + L9) `) + (L9 `)) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
((L9 + x) `) + L9 is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + L9) ` is M2( the U1 of c<sub>1</sub>)
((((L9 + x) `) + L9) `) + x is M2( the U1 of c<sub>1</sub>)
x ` is M2( the U1 of c₁)
(x `) ` is M2( the U1 of c₁)
(((((L9 + x) `) + L9) `) + x) ` is M2( the U1 of c<sub>1</sub>)
((((((L9 + x) `) + L9) `) + x) `) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
((L9 + x) `) ` is M2( the U1 of c₁)
x + L9 is M2( the U1 of c₁)
(x + L9) ` is M2( the U1 of c<sub>1</sub>)
((x + L9) `) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
x + y is M2( the U1 of c<sub>1</sub>)
(x + y) ` is M2( the U1 of c₁)
x + L9 is M2( the U1 of c₁)
(x + L9) ` is M2( the U1 of c<sub>1</sub>)
((x + y) `) + ((x + L9) `) is M2( the U1 of c<sub>1</sub>)
(((x + y) `) + ((x + L9) `)) ` is M2( the U1 of c₁)
L9 + ((((x + y) `) + ((x + L9) `)) `) is M2( the U1 of c<sub>1</sub>)
((x + L9) `) ` is M2( the U1 of c<sub>1</sub>)
(L9 + ((((x + y) `) + ((x + L9) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
((L9 + ((((x + y) `) + ((x + L9) `)) `)) `) ` is M2( the U1 of c₁)
c₁ is non empty () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
L9 + x is M2( the U1 of c₁)
x + L9 is M2( the U1 of c₁)
(L9 + x) ` is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
x + L9 is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty ComplLLattStr
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
((L9 + x) `) + L9 is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + L9) ` is M2( the U1 of c<sub>1</sub>)
((((L9 + x) `) + L9) `) + x is M2( the U1 of c<sub>1</sub>)
x ` is M2( the U1 of c₁)
(x `) ` is M2( the U1 of c₁)
c₁ is non empty join-commutative () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
L9 + x is M2( the U1 of c₁)
(L9 + x) ` is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) + x is M2( the U1 of c₁)
(((L9 + x) `) + x) ` is M2( the U1 of c₁)
((((L9 + x) `) + x) `) + L9 is M2( the U1 of c₁)
c₁ is non empty join-commutative () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
x + L9 is M2( the U1 of c₁)
(x + L9) ` is M2( the U1 of c<sub>1</sub>)
((x + L9) `) + x is M2( the U1 of c₁)
(((x + L9) `) + x) ` is M2( the U1 of c₁)
L9 + ((((x + L9) `) + x) `) is M2( the U1 of c₁)
c₁ is non empty join-commutative () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
L9 + (x `) is M2( the U1 of c₁)
(L9 + (x `)) ` is M2( the U1 of c₁)
(x `) + x is M2( the U1 of c<sub>1</sub>)
((x `) + x) ` is M2( the U1 of c<sub>1</sub>)
((L9 + (x `)) `) + (((x `) + x) `) is M2( the U1 of c<sub>1</sub>)
x + ((L9 + (x `)) `) is M2( the U1 of c<sub>1</sub>)
(x + ((L9 + (x `)) `)) ` is M2( the U1 of c₁)
((x + ((L9 + (x `)) `)) `) + x is M2( the U1 of c<sub>1</sub>)
(((x + ((L9 + (x `)) `)) `) + x) ` is M2( the U1 of c<sub>1</sub>)
((L9 + (x `)) `) + ((((x + ((L9 + (x `)) `)) `) + x) `) is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
x + (x `) is M2( the U1 of c₁)
(x + (x `)) ` is M2( the U1 of c₁)
((L9 + x) `) + ((x + (x `)) `) is M2( the U1 of c<sub>1</sub>)
(x `) + ((L9 + x) `) is M2( the U1 of c<sub>1</sub>)
((x `) + ((L9 + x) `)) ` is M2( the U1 of c₁)
(((x `) + ((L9 + x) `)) `) + (x `) is M2( the U1 of c₁)
((((x `) + ((L9 + x) `)) `) + (x `)) ` is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) + (((((x `) + ((L9 + x) `)) `) + (x `)) `) is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
(x `) + x is M2( the U1 of c₁)
((x `) + x) ` is M2( the U1 of c₁)
((L9 + x) `) + (((x `) + x) `) is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
x ` is M2( the U1 of c₁)
L9 + (x `) is M2( the U1 of c<sub>1</sub>)
(L9 + (x `)) ` is M2( the U1 of c<sub>1</sub>)
((L9 + (x `)) `) ` is M2( the U1 of c₁)
(((L9 + (x `)) `) `) + x is M2( the U1 of c<sub>1</sub>)
((((L9 + (x `)) `) `) + x) ` is M2( the U1 of c<sub>1</sub>)
(x `) + x is M2( the U1 of c₁)
((x `) + x) ` is M2( the U1 of c₁)
((L9 + (x `)) `) + (((x `) + x) `) is M2( the U1 of c₁)
(((L9 + (x `)) `) + (((x `) + x) `)) ` is M2( the U1 of c<sub>1</sub>)
((((L9 + (x `)) `) + (((x `) + x) `)) `) + x is M2( the U1 of c₁)
(((((L9 + (x `)) `) + (((x `) + x) `)) `) + x) ` is M2( the U1 of c₁)
c₁ is non empty join-commutative () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
L9 + (x `) is M2( the U1 of c₁)
(L9 + (x `)) + x is M2( the U1 of c<sub>1</sub>)
((L9 + (x `)) + x) ` is M2( the U1 of c<sub>1</sub>)
(x `) + x is M2( the U1 of c₁)
((x `) + x) ` is M2( the U1 of c₁)
(L9 + (x `)) ` is M2( the U1 of c₁)
((L9 + (x `)) `) ` is M2( the U1 of c<sub>1</sub>)
(((L9 + (x `)) `) `) + x is M2( the U1 of c₁)
((((L9 + (x `)) `) `) + x) ` is M2( the U1 of c₁)
c₁ is non empty join-commutative () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
L9 + (x `) is M2( the U1 of c₁)
y is M2( the U1 of c₁)
(L9 + (x `)) + y is M2( the U1 of c<sub>1</sub>)
((L9 + (x `)) + y) ` is M2( the U1 of c<sub>1</sub>)
(((L9 + (x `)) + y) `) + x is M2( the U1 of c<sub>1</sub>)
((((L9 + (x `)) + y) `) + x) ` is M2( the U1 of c₁)
(x `) + x is M2( the U1 of c<sub>1</sub>)
((x `) + x) ` is M2( the U1 of c<sub>1</sub>)
(((((L9 + (x `)) + y) `) + x) `) + (((x `) + x) `) is M2( the U1 of c₁)
((((((L9 + (x `)) + y) `) + x) `) + (((x `) + x) `)) ` is M2( the U1 of c₁)
(L9 + (x `)) + x is M2( the U1 of c<sub>1</sub>)
((L9 + (x `)) + x) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
x + y is M2( the U1 of c<sub>1</sub>)
(x + y) ` is M2( the U1 of c₁)
x + L9 is M2( the U1 of c₁)
(x + L9) ` is M2( the U1 of c<sub>1</sub>)
((x + y) `) + ((x + L9) `) is M2( the U1 of c<sub>1</sub>)
(((x + y) `) + ((x + L9) `)) ` is M2( the U1 of c₁)
L9 + ((((x + y) `) + ((x + L9) `)) `) is M2( the U1 of c<sub>1</sub>)
((x + L9) `) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
y + x is M2( the U1 of c<sub>1</sub>)
(y + x) ` is M2( the U1 of c₁)
((y + x) `) + L9 is M2( the U1 of c<sub>1</sub>)
(((y + x) `) + L9) ` is M2( the U1 of c<sub>1</sub>)
x + ((((y + x) `) + L9) `) is M2( the U1 of c<sub>1</sub>)
(x + ((((y + x) `) + L9) `)) ` is M2( the U1 of c₁)
L9 + ((x + ((((y + x) `) + L9) `)) `) is M2( the U1 of c<sub>1</sub>)
x ` is M2( the U1 of c₁)
((y + x) `) + (x `) is M2( the U1 of c₁)
(((y + x) `) + (x `)) ` is M2( the U1 of c<sub>1</sub>)
((((y + x) `) + (x `)) `) + ((((y + x) `) + L9) `) is M2( the U1 of c₁)
(((((y + x) `) + (x `)) `) + ((((y + x) `) + L9) `)) ` is M2( the U1 of c₁)
L9 + ((((((y + x) `) + (x `)) `) + ((((y + x) `) + L9) `)) `) is M2( the U1 of c₁)
c₁ is non empty join-commutative () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
x + L9 is M2( the U1 of c₁)
(x + L9) ` is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
x + y is M2( the U1 of c<sub>1</sub>)
(x + y) ` is M2( the U1 of c₁)
((x + L9) `) + ((x + y) `) is M2( the U1 of c₁)
(((x + L9) `) + ((x + y) `)) ` is M2( the U1 of c<sub>1</sub>)
L9 + ((((x + L9) `) + ((x + y) `)) `) is M2( the U1 of c₁)
c₁ is non empty join-commutative () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
L9 + x is M2( the U1 of c₁)
(L9 + x) ` is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
L9 + y is M2( the U1 of c<sub>1</sub>)
(L9 + y) ` is M2( the U1 of c₁)
((L9 + x) `) + ((L9 + y) `) is M2( the U1 of c₁)
(((L9 + x) `) + ((L9 + y) `)) ` is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) + ((((L9 + x) `) + ((L9 + y) `)) `) is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + ((((L9 + x) `) + ((L9 + y) `)) `)) ` is M2( the U1 of c₁)
((((L9 + x) `) + ((((L9 + x) `) + ((L9 + y) `)) `)) `) + x is M2( the U1 of c<sub>1</sub>)
x + ((((L9 + x) `) + ((L9 + y) `)) `) is M2( the U1 of c₁)
(x + ((((L9 + x) `) + ((L9 + y) `)) `)) ` is M2( the U1 of c₁)
((x + ((((L9 + x) `) + ((L9 + y) `)) `)) `) + ((((L9 + x) `) + ((L9 + y) `)) `) is M2( the U1 of c<sub>1</sub>)
(((x + ((((L9 + x) `) + ((L9 + y) `)) `)) `) + ((((L9 + x) `) + ((L9 + y) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
((((x + ((((L9 + x) `) + ((L9 + y) `)) `)) `) + ((((L9 + x) `) + ((L9 + y) `)) `)) `) + x is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
x ` is M2( the U1 of c₁)
L9 + (x `) is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
(L9 + (x `)) + y is M2( the U1 of c₁)
((L9 + (x `)) + y) ` is M2( the U1 of c₁)
(((L9 + (x `)) + y) `) + x is M2( the U1 of c₁)
((((L9 + (x `)) + y) `) + x) ` is M2( the U1 of c<sub>1</sub>)
(((((L9 + (x `)) + y) `) + x) `) ` is M2( the U1 of c<sub>1</sub>)
(x `) + x is M2( the U1 of c₁)
((x `) + x) ` is M2( the U1 of c₁)
(((((L9 + (x `)) + y) `) + x) `) + (((x `) + x) `) is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
x + (L9 `) is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
(x + (L9 `)) + y is M2( the U1 of c₁)
((x + (L9 `)) + y) ` is M2( the U1 of c₁)
L9 + (((x + (L9 `)) + y) `) is M2( the U1 of c₁)
(((x + (L9 `)) + y) `) + L9 is M2( the U1 of c₁)
((((x + (L9 `)) + y) `) + L9) ` is M2( the U1 of c<sub>1</sub>)
(((((x + (L9 `)) + y) `) + L9) `) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
x is M2( the U1 of c₁)
x + L9 is M2( the U1 of c₁)
y is M2( the U1 of c₁)
(x + L9) + y is M2( the U1 of c₁)
((x + L9) + y) ` is M2( the U1 of c<sub>1</sub>)
(L9 `) + (((x + L9) + y) `) is M2( the U1 of c<sub>1</sub>)
(L9 `) ` is M2( the U1 of c<sub>1</sub>)
x + ((L9 `) `) is M2( the U1 of c<sub>1</sub>)
(x + ((L9 `) `)) + y is M2( the U1 of c<sub>1</sub>)
((x + ((L9 `) `)) + y) ` is M2( the U1 of c₁)
(L9 `) + (((x + ((L9 `) `)) + y) `) is M2( the U1 of c₁)
c₁ is non empty join-commutative () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
L9 + x is M2( the U1 of c₁)
(L9 + x) ` is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) + L9 is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
L9 + (x `) is M2( the U1 of c₁)
(((L9 + x) `) + L9) ` is M2( the U1 of c₁)
x + ((((L9 + x) `) + L9) `) is M2( the U1 of c₁)
(x + ((((L9 + x) `) + L9) `)) ` is M2( the U1 of c<sub>1</sub>)
L9 + ((x + ((((L9 + x) `) + L9) `)) `) is M2( the U1 of c₁)
c₁ is non empty join-commutative () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
L9 + (x `) is M2( the U1 of c₁)
(L9 + (x `)) ` is M2( the U1 of c₁)
L9 + ((L9 + (x `)) `) is M2( the U1 of c₁)
(L9 + ((L9 + (x `)) `)) ` is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
((L9 + x) `) + L9 is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + L9) ` is M2( the U1 of c<sub>1</sub>)
L9 + ((((L9 + x) `) + L9) `) is M2( the U1 of c<sub>1</sub>)
(L9 + ((((L9 + x) `) + L9) `)) ` is M2( the U1 of c₁)
c₁ is non empty join-commutative () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
L9 + x is M2( the U1 of c₁)
(L9 + x) ` is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
L9 + y is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) + (L9 + y) is M2( the U1 of c₁)
(((L9 + x) `) + (L9 + y)) ` is M2( the U1 of c₁)
((((L9 + x) `) + (L9 + y)) `) + x is M2( the U1 of c₁)
(L9 + y) ` is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) + ((L9 + y) `) is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + ((L9 + y) `)) ` is M2( the U1 of c₁)
((L9 + x) `) + ((((L9 + x) `) + ((L9 + y) `)) `) is M2( the U1 of c₁)
(((L9 + x) `) + ((((L9 + x) `) + ((L9 + y) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
y is M2( the U1 of c₁)
((L9 + x) `) + y is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + y) ` is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
(L9 `) + x is M2( the U1 of c<sub>1</sub>)
((L9 `) + x) ` is M2( the U1 of c<sub>1</sub>)
((((L9 + x) `) + y) `) + (((L9 `) + x) `) is M2( the U1 of c<sub>1</sub>)
(((((L9 + x) `) + y) `) + (((L9 `) + x) `)) ` is M2( the U1 of c₁)
((((((L9 + x) `) + y) `) + (((L9 `) + x) `)) `) + x is M2( the U1 of c<sub>1</sub>)
(((L9 `) + x) `) ` is M2( the U1 of c₁)
(((((((L9 + x) `) + y) `) + (((L9 `) + x) `)) `) + x) ` is M2( the U1 of c₁)
((((((((L9 + x) `) + y) `) + (((L9 `) + x) `)) `) + x) `) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
y is M2( the U1 of c₁)
((L9 + x) `) + y is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + y) ` is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
(L9 `) + x is M2( the U1 of c<sub>1</sub>)
((L9 `) + x) ` is M2( the U1 of c<sub>1</sub>)
((((L9 + x) `) + y) `) + (((L9 `) + x) `) is M2( the U1 of c<sub>1</sub>)
(((((L9 + x) `) + y) `) + (((L9 `) + x) `)) ` is M2( the U1 of c₁)
((((((L9 + x) `) + y) `) + (((L9 `) + x) `)) `) + x is M2( the U1 of c<sub>1</sub>)
(((L9 `) + x) `) ` is M2( the U1 of c₁)
c₁ is non empty join-commutative () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
L9 ` is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
x + L9 is M2( the U1 of c<sub>1</sub>)
(x + L9) ` is M2( the U1 of c₁)
((x + L9) `) ` is M2( the U1 of c₁)
y is M2( the U1 of c₁)
x + y is M2( the U1 of c₁)
(((x + L9) `) `) + (x + y) is M2( the U1 of c₁)
((((x + L9) `) `) + (x + y)) ` is M2( the U1 of c<sub>1</sub>)
(L9 `) + (((((x + L9) `) `) + (x + y)) `) is M2( the U1 of c<sub>1</sub>)
((L9 `) + (((((x + L9) `) `) + (x + y)) `)) ` is M2( the U1 of c₁)
(((L9 `) + (((((x + L9) `) `) + (x + y)) `)) `) + (x + y) is M2( the U1 of c<sub>1</sub>)
((x + L9) `) + (x + y) is M2( the U1 of c₁)
(((x + L9) `) + (x + y)) ` is M2( the U1 of c₁)
((((x + L9) `) + (x + y)) `) + L9 is M2( the U1 of c₁)
(((((x + L9) `) + (x + y)) `) + L9) ` is M2( the U1 of c<sub>1</sub>)
((((((x + L9) `) + (x + y)) `) + L9) `) + (((((x + L9) `) `) + (x + y)) `) is M2( the U1 of c<sub>1</sub>)
(((((((x + L9) `) + (x + y)) `) + L9) `) + (((((x + L9) `) `) + (x + y)) `)) ` is M2( the U1 of c₁)
((((((((x + L9) `) + (x + y)) `) + L9) `) + (((((x + L9) `) `) + (x + y)) `)) `) + (x + y) is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
x is M2( the U1 of c₁)
x + L9 is M2( the U1 of c₁)
y is M2( the U1 of c₁)
x + y is M2( the U1 of c₁)
(x + L9) + (x + y) is M2( the U1 of c₁)
((x + L9) + (x + y)) ` is M2( the U1 of c<sub>1</sub>)
(L9 `) + (((x + L9) + (x + y)) `) is M2( the U1 of c<sub>1</sub>)
((L9 `) + (((x + L9) + (x + y)) `)) ` is M2( the U1 of c₁)
(((L9 `) + (((x + L9) + (x + y)) `)) `) + (x + y) is M2( the U1 of c<sub>1</sub>)
(x + L9) ` is M2( the U1 of c₁)
((x + L9) `) ` is M2( the U1 of c₁)
(((x + L9) `) `) + (x + y) is M2( the U1 of c₁)
((((x + L9) `) `) + (x + y)) ` is M2( the U1 of c<sub>1</sub>)
(L9 `) + (((((x + L9) `) `) + (x + y)) `) is M2( the U1 of c<sub>1</sub>)
((L9 `) + (((((x + L9) `) `) + (x + y)) `)) ` is M2( the U1 of c₁)
(((L9 `) + (((((x + L9) `) `) + (x + y)) `)) `) + (x + y) is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
x is M2( the U1 of c₁)
x + L9 is M2( the U1 of c₁)
y is M2( the U1 of c₁)
x + y is M2( the U1 of c₁)
(x + L9) + (x + y) is M2( the U1 of c₁)
((x + L9) + (x + y)) ` is M2( the U1 of c<sub>1</sub>)
(L9 `) + (((x + L9) + (x + y)) `) is M2( the U1 of c<sub>1</sub>)
((L9 `) + (((x + L9) + (x + y)) `)) ` is M2( the U1 of c₁)
(((L9 `) + (((x + L9) + (x + y)) `)) `) + (x + y) is M2( the U1 of c<sub>1</sub>)
(x + L9) ` is M2( the U1 of c₁)
((x + L9) `) ` is M2( the U1 of c₁)
(((x + L9) `) `) + (x + y) is M2( the U1 of c₁)
c₁ is non empty join-commutative () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
L9 ` is M2( the U1 of c<sub>1</sub>)
(L9 `) ` is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
x + y is M2( the U1 of c<sub>1</sub>)
((L9 `) `) + (x + y) is M2( the U1 of c<sub>1</sub>)
x + L9 is M2( the U1 of c<sub>1</sub>)
(x + L9) + (x + y) is M2( the U1 of c<sub>1</sub>)
((x + L9) + (x + y)) ` is M2( the U1 of c₁)
(L9 `) + (((x + L9) + (x + y)) `) is M2( the U1 of c₁)
c₁ is non empty join-commutative () ComplLLattStr
the U1 of c₁ is V11() set
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
L9 + x is M2( the U1 of c₁)
y is M2( the U1 of c₁)
L9 + y is M2( the U1 of c₁)
(L9 + x) + (L9 + y) is M2( the U1 of c₁)
x + (L9 + y) is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
(x `) ` is M2( the U1 of c<sub>1</sub>)
((x `) `) + (L9 + y) is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
L9 + y is M2( the U1 of c<sub>1</sub>)
(L9 + x) + (L9 + y) is M2( the U1 of c<sub>1</sub>)
y + (L9 + x) is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
x + y is M2( the U1 of c<sub>1</sub>)
L9 + (x + y) is M2( the U1 of c<sub>1</sub>)
x + L9 is M2( the U1 of c<sub>1</sub>)
y + (x + L9) is M2( the U1 of c<sub>1</sub>)
(x + L9) + (x + y) is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
x + y is M2( the U1 of c<sub>1</sub>)
L9 + (x + y) is M2( the U1 of c<sub>1</sub>)
y + L9 is M2( the U1 of c<sub>1</sub>)
x + (y + L9) is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
(L9 + x) + y is M2( the U1 of c<sub>1</sub>)
x + y is M2( the U1 of c<sub>1</sub>)
L9 + (x + y) is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
(L9 + x) + y is M2( the U1 of c<sub>1</sub>)
x + y is M2( the U1 of c<sub>1</sub>)
L9 + (x + y) is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty join-commutative () ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
L9 + (x `) is M2( the U1 of c₁)
(L9 + (x `)) ` is M2( the U1 of c₁)
((L9 + x) `) + ((L9 + (x `)) `) is M2( the U1 of c<sub>1</sub>)
(((L9 + x) `) + ((L9 + (x `)) `)) ` is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty ComplLLattStr
c<sub>1</sub> is non empty ComplLLattStr
c<sub>1</sub> is non empty ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
x is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
x + L9 is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
x + (L9 `) is M2( the U1 of c<sub>1</sub>)
(x + L9) *' (x + (L9 `)) is M2( the U1 of c₁)
y is non empty join-commutative join-associative upper-bounded Huntington join-idempotent ComplLLattStr
the U1 of y is V11() set
z is M2( the U1 of y)
Z is M2( the U1 of y)
z + Z is M2( the U1 of y)
Z ` is M2( the U1 of y)
z + (Z `) is M2( the U1 of y)
(z + Z) *' (z + (Z `)) is M2( the U1 of y)
Z *' (Z `) is M2( the U1 of y)
z + (Z *' (Z `)) is M2( the U1 of y)
Bot y is M2( the U1 of y)
z + (Bot y) is M2( the U1 of y)
c<sub>1</sub> is non empty join-commutative join-associative ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
x is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
x + y is M2( the U1 of c<sub>1</sub>)
(x + y) ` is M2( the U1 of c₁)
z is M2( the U1 of c₁)
((x + y) `) + z is M2( the U1 of c<sub>1</sub>)
(((x + y) `) + z) ` is M2( the U1 of c<sub>1</sub>)
z ` is M2( the U1 of c₁)
Z is M2( the U1 of c₁)
z + Z is M2( the U1 of c₁)
(z + Z) ` is M2( the U1 of c<sub>1</sub>)
(z `) + ((z + Z) `) is M2( the U1 of c<sub>1</sub>)
((z `) + ((z + Z) `)) ` is M2( the U1 of c₁)
x + (((z `) + ((z + Z) `)) `) is M2( the U1 of c<sub>1</sub>)
(x + (((z `) + ((z + Z) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
((((x + y) `) + z) `) + ((x + (((z `) + ((z + Z) `)) `)) `) is M2( the U1 of c<sub>1</sub>)
(((((x + y) `) + z) `) + ((x + (((z `) + ((z + Z) `)) `)) `)) ` is M2( the U1 of c₁)
L9 is non empty join-commutative join-associative upper-bounded Robbins Huntington join-idempotent ComplLLattStr
z + x is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
z + (x `) is M2( the U1 of c₁)
(z + x) *' (z + (x `)) is M2( the U1 of c<sub>1</sub>)
x + y is M2( the U1 of c<sub>1</sub>)
(x + y) ` is M2( the U1 of c₁)
((x + y) `) + z is M2( the U1 of c<sub>1</sub>)
(((x + y) `) + z) *' z is M2( the U1 of c₁)
z + ((x + y) `) is M2( the U1 of c<sub>1</sub>)
(z + ((x + y) `)) *' z is M2( the U1 of c₁)
z *' (z + ((x + y) `)) is M2( the U1 of c<sub>1</sub>)
(((x + y) `) + z) *' x is M2( the U1 of c₁)
((((x + y) `) + z) *' x) + z is M2( the U1 of c<sub>1</sub>)
z + ((((x + y) `) + z) *' x) is M2( the U1 of c₁)
z + (((x + y) `) + z) is M2( the U1 of c<sub>1</sub>)
(z + (((x + y) `) + z)) *' (z + x) is M2( the U1 of c₁)
(((x + y) `) + z) + z is M2( the U1 of c<sub>1</sub>)
((((x + y) `) + z) + z) *' (z + x) is M2( the U1 of c₁)
z + z is M2( the U1 of c₁)
((x + y) `) + (z + z) is M2( the U1 of c<sub>1</sub>)
(((x + y) `) + (z + z)) *' (z + x) is M2( the U1 of c₁)
(((x + y) `) + z) *' (z + x) is M2( the U1 of c<sub>1</sub>)
y ` is M2( the U1 of c₁)
(x `) *' (y `) is M2( the U1 of c₁)
((x `) *' (y `)) ` is M2( the U1 of c<sub>1</sub>)
(((x `) *' (y `)) `) ` is M2( the U1 of c<sub>1</sub>)
((((x `) *' (y `)) `) `) + z is M2( the U1 of c<sub>1</sub>)
(((((x `) *' (y `)) `) `) + z) *' (z + x) is M2( the U1 of c<sub>1</sub>)
((x `) *' (y `)) + z is M2( the U1 of c<sub>1</sub>)
(((x `) *' (y `)) + z) *' (z + x) is M2( the U1 of c<sub>1</sub>)
z + ((x `) *' (y `)) is M2( the U1 of c<sub>1</sub>)
(z + ((x `) *' (y `))) *' (z + x) is M2( the U1 of c<sub>1</sub>)
z + (y `) is M2( the U1 of c₁)
(z + (x `)) *' (z + (y `)) is M2( the U1 of c₁)
((z + (x `)) *' (z + (y `))) *' (z + x) is M2( the U1 of c₁)
(z + x) *' ((z + (x `)) *' (z + (y `))) is M2( the U1 of c₁)
(x `) + z is M2( the U1 of c<sub>1</sub>)
((x `) + z) *' (z + (y `)) is M2( the U1 of c<sub>1</sub>)
(z + x) *' (((x `) + z) *' (z + (y `))) is M2( the U1 of c<sub>1</sub>)
(y `) + z is M2( the U1 of c₁)
((x `) + z) *' ((y `) + z) is M2( the U1 of c₁)
(z + x) *' (((x `) + z) *' ((y `) + z)) is M2( the U1 of c₁)
(z + x) *' ((x `) + z) is M2( the U1 of c<sub>1</sub>)
((z + x) *' ((x `) + z)) *' ((y `) + z) is M2( the U1 of c<sub>1</sub>)
((z + x) *' (z + (x `))) *' ((y `) + z) is M2( the U1 of c<sub>1</sub>)
z *' (z + (y `)) is M2( the U1 of c₁)
(((x + y) `) + z) ` is M2( the U1 of c₁)
z + Z is M2( the U1 of c₁)
(z + Z) ` is M2( the U1 of c<sub>1</sub>)
(z `) + ((z + Z) `) is M2( the U1 of c<sub>1</sub>)
((z `) + ((z + Z) `)) ` is M2( the U1 of c₁)
x + (((z `) + ((z + Z) `)) `) is M2( the U1 of c<sub>1</sub>)
(x + (((z `) + ((z + Z) `)) `)) ` is M2( the U1 of c<sub>1</sub>)
((((x + y) `) + z) `) + ((x + (((z `) + ((z + Z) `)) `)) `) is M2( the U1 of c<sub>1</sub>)
(((((x + y) `) + z) `) + ((x + (((z `) + ((z + Z) `)) `)) `)) ` is M2( the U1 of c₁)
((((x + y) `) + z) `) ` is M2( the U1 of c<sub>1</sub>)
((x + (((z `) + ((z + Z) `)) `)) `) ` is M2( the U1 of c₁)
(((((x + y) `) + z) `) `) *' (((x + (((z `) + ((z + Z) `)) `)) `) `) is M2( the U1 of c₁)
((((((x + y) `) + z) `) `) *' (((x + (((z `) + ((z + Z) `)) `)) `) `)) ` is M2( the U1 of c<sub>1</sub>)
(((((((x + y) `) + z) `) `) *' (((x + (((z `) + ((z + Z) `)) `)) `) `)) `) ` is M2( the U1 of c<sub>1</sub>)
(((((x + y) `) + z) `) `) *' (x + (((z `) + ((z + Z) `)) `)) is M2( the U1 of c<sub>1</sub>)
(((x + y) `) + z) *' (x + (((z `) + ((z + Z) `)) `)) is M2( the U1 of c<sub>1</sub>)
((x + y) `) ` is M2( the U1 of c<sub>1</sub>)
(((x + y) `) `) *' (z `) is M2( the U1 of c₁)
((((x + y) `) `) *' (z `)) ` is M2( the U1 of c₁)
(((((x + y) `) `) *' (z `)) `) *' (x + (((z `) + ((z + Z) `)) `)) is M2( the U1 of c<sub>1</sub>)
(x + y) *' (z `) is M2( the U1 of c₁)
((x + y) *' (z `)) ` is M2( the U1 of c₁)
(((x + y) *' (z `)) `) *' (x + (((z `) + ((z + Z) `)) `)) is M2( the U1 of c<sub>1</sub>)
(z `) ` is M2( the U1 of c<sub>1</sub>)
((z + Z) `) ` is M2( the U1 of c<sub>1</sub>)
((z `) `) *' (((z + Z) `) `) is M2( the U1 of c<sub>1</sub>)
(((z `) `) *' (((z + Z) `) `)) ` is M2( the U1 of c₁)
((((z `) `) *' (((z + Z) `) `)) `) ` is M2( the U1 of c₁)
x + (((((z `) `) *' (((z + Z) `) `)) `) `) is M2( the U1 of c₁)
(((x + y) *' (z `)) `) *' (x + (((((z `) `) *' (((z + Z) `) `)) `) `)) is M2( the U1 of c₁)
z *' (((z + Z) `) `) is M2( the U1 of c₁)
(z *' (((z + Z) `) `)) ` is M2( the U1 of c<sub>1</sub>)
((z *' (((z + Z) `) `)) `) ` is M2( the U1 of c<sub>1</sub>)
x + (((z *' (((z + Z) `) `)) `) `) is M2( the U1 of c<sub>1</sub>)
(((x + y) *' (z `)) `) *' (x + (((z *' (((z + Z) `) `)) `) `)) is M2( the U1 of c<sub>1</sub>)
x + (z *' (((z + Z) `) `)) is M2( the U1 of c<sub>1</sub>)
(((x + y) *' (z `)) `) *' (x + (z *' (((z + Z) `) `))) is M2( the U1 of c<sub>1</sub>)
z *' (z + Z) is M2( the U1 of c<sub>1</sub>)
x + (z *' (z + Z)) is M2( the U1 of c<sub>1</sub>)
(((x + y) *' (z `)) `) *' (x + (z *' (z + Z))) is M2( the U1 of c<sub>1</sub>)
x + z is M2( the U1 of c<sub>1</sub>)
(((x + y) *' (z `)) `) *' (x + z) is M2( the U1 of c<sub>1</sub>)
(((x + y) *' (z `)) `) *' x is M2( the U1 of c<sub>1</sub>)
(((x + y) *' (z `)) `) *' z is M2( the U1 of c<sub>1</sub>)
((((x + y) *' (z `)) `) *' x) + ((((x + y) *' (z `)) `) *' z) is M2( the U1 of c<sub>1</sub>)
(((((x + y) `) `) *' (z `)) `) *' x is M2( the U1 of c<sub>1</sub>)
((((((x + y) `) `) *' (z `)) `) *' x) + ((((x + y) *' (z `)) `) *' z) is M2( the U1 of c<sub>1</sub>)
((((x + y) `) + z) *' x) + ((((x + y) *' (z `)) `) *' z) is M2( the U1 of c₁)
(((((x + y) `) `) *' (z `)) `) *' z is M2( the U1 of c₁)
((((x + y) `) + z) *' x) + ((((((x + y) `) `) *' (z `)) `) *' z) is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty ComplLLattStr
c<sub>1</sub> is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like OrthoLattStr
c<sub>1</sub> is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like well-complemented OrthoLattStr
c<sub>1</sub> is non empty ComplLLattStr
the U1 of c<sub>1</sub> is V11() set
L9 is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
x is M2( the U1 of c₁)
(L9 `) + x is M2( the U1 of c<sub>1</sub>)
(L9 `) + ((L9 `) + x) is M2( the U1 of c<sub>1</sub>)
((L9 `) + x) ` is M2( the U1 of c<sub>1</sub>)
(((L9 `) + x) `) + L9 is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
x is M2( the U1 of c₁)
(L9 `) + x is M2( the U1 of c<sub>1</sub>)
((L9 `) + x) ` is M2( the U1 of c<sub>1</sub>)
(((L9 `) + x) `) + x is M2( the U1 of c<sub>1</sub>)
x + L9 is M2( the U1 of c<sub>1</sub>)
(((L9 `) + x) `) + ((((L9 `) + x) `) + x) is M2( the U1 of c<sub>1</sub>)
(((L9 `) + x) `) + L9 is M2( the U1 of c<sub>1</sub>)
x + ((((L9 `) + x) `) + L9) is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
L9 + L9 is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
(L9 `) + L9 is M2( the U1 of c<sub>1</sub>)
((L9 `) + L9) ` is M2( the U1 of c<sub>1</sub>)
(((L9 `) + L9) `) + L9 is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
L9 + (L9 + x) is M2( the U1 of c<sub>1</sub>)
x ` is M2( the U1 of c₁)
(x `) + L9 is M2( the U1 of c<sub>1</sub>)
((x `) + L9) ` is M2( the U1 of c<sub>1</sub>)
L9 + L9 is M2( the U1 of c<sub>1</sub>)
(((x `) + L9) `) + (L9 + L9) is M2( the U1 of c<sub>1</sub>)
(((x `) + L9) `) + L9 is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) + x is M2( the U1 of c<sub>1</sub>)
x ` is M2( the U1 of c₁)
(x `) + (L9 + x) is M2( the U1 of c<sub>1</sub>)
((x `) + (L9 + x)) ` is M2( the U1 of c<sub>1</sub>)
(((x `) + (L9 + x)) `) + (L9 + x) is M2( the U1 of c<sub>1</sub>)
L9 + (L9 + x) is M2( the U1 of c<sub>1</sub>)
(((x `) + (L9 + x)) `) + (L9 + (L9 + x)) is M2( the U1 of c<sub>1</sub>)
(L9 + x) + (L9 + x) is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) + L9 is M2( the U1 of c<sub>1</sub>)
x ` is M2( the U1 of c₁)
(x `) + L9 is M2( the U1 of c<sub>1</sub>)
((x `) + L9) ` is M2( the U1 of c<sub>1</sub>)
(((x `) + L9) `) + L9 is M2( the U1 of c<sub>1</sub>)
((((x `) + L9) `) + L9) + L9 is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
x + L9 is M2( the U1 of c<sub>1</sub>)
x + (x + L9) is M2( the U1 of c<sub>1</sub>)
L9 + (x + (x + L9)) is M2( the U1 of c<sub>1</sub>)
(x + L9) ` is M2( the U1 of c₁)
((x + L9) `) + L9 is M2( the U1 of c<sub>1</sub>)
(((x + L9) `) + L9) ` is M2( the U1 of c<sub>1</sub>)
((((x + L9) `) + L9) `) + (x + L9) is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
x + L9 is M2( the U1 of c<sub>1</sub>)
L9 + (x + L9) is M2( the U1 of c<sub>1</sub>)
x + (x + L9) is M2( the U1 of c<sub>1</sub>)
L9 + (x + (x + L9)) is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
x ` is M2( the U1 of c₁)
L9 + (x `) is M2( the U1 of c<sub>1</sub>)
(L9 + (x `)) ` is M2( the U1 of c<sub>1</sub>)
((L9 + (x `)) `) + x is M2( the U1 of c<sub>1</sub>)
(x `) + (L9 + (x `)) is M2( the U1 of c<sub>1</sub>)
((x `) + (L9 + (x `))) ` is M2( the U1 of c₁)
(((x `) + (L9 + (x `))) `) + x is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
(L9 `) ` is M2( the U1 of c₁)
((L9 `) `) + L9 is M2( the U1 of c₁)
(L9 `) + (L9 `) is M2( the U1 of c₁)
((L9 `) + (L9 `)) ` is M2( the U1 of c<sub>1</sub>)
(((L9 `) + (L9 `)) `) + L9 is M2( the U1 of c₁)
L9 is M2( the U1 of c₁)
L9 ` is M2( the U1 of c<sub>1</sub>)
(L9 `) ` is M2( the U1 of c<sub>1</sub>)
L9 + ((L9 `) `) is M2( the U1 of c<sub>1</sub>)
((L9 `) `) + L9 is M2( the U1 of c<sub>1</sub>)
(((L9 `) `) + L9) + ((L9 `) `) is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
(L9 `) ` is M2( the U1 of c₁)
x is M2( the U1 of c₁)
((L9 `) `) + x is M2( the U1 of c₁)
L9 + (((L9 `) `) + x) is M2( the U1 of c₁)
L9 + x is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
(x `) + L9 is M2( the U1 of c₁)
((x `) + L9) ` is M2( the U1 of c₁)
((L9 `) `) + L9 is M2( the U1 of c₁)
(((x `) + L9) `) + (((L9 `) `) + L9) is M2( the U1 of c₁)
(((x `) + L9) `) + L9 is M2( the U1 of c₁)
L9 is M2( the U1 of c₁)
L9 ` is M2( the U1 of c<sub>1</sub>)
(L9 `) ` is M2( the U1 of c<sub>1</sub>)
((L9 `) `) ` is M2( the U1 of c₁)
(((L9 `) `) `) ` is M2( the U1 of c₁)
L9 + ((((L9 `) `) `) `) is M2( the U1 of c₁)
((L9 `) `) + ((((L9 `) `) `) `) is M2( the U1 of c₁)
L9 + (((L9 `) `) + ((((L9 `) `) `) `)) is M2( the U1 of c₁)
L9 + ((L9 `) `) is M2( the U1 of c₁)
L9 is M2( the U1 of c₁)
L9 ` is M2( the U1 of c<sub>1</sub>)
(L9 `) ` is M2( the U1 of c<sub>1</sub>)
((L9 `) `) ` is M2( the U1 of c₁)
(((L9 `) `) `) ` is M2( the U1 of c₁)
L9 + ((((L9 `) `) `) `) is M2( the U1 of c₁)
(L9 + ((((L9 `) `) `) `)) ` is M2( the U1 of c<sub>1</sub>)
((L9 + ((((L9 `) `) `) `)) `) + (((L9 `) `) `) is M2( the U1 of c<sub>1</sub>)
(L9 `) + (((L9 `) `) `) is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
x is M2( the U1 of c₁)
(L9 `) + x is M2( the U1 of c<sub>1</sub>)
((L9 `) + x) ` is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
(L9 `) + y is M2( the U1 of c₁)
((L9 `) + y) ` is M2( the U1 of c₁)
(((L9 `) + y) `) + x is M2( the U1 of c₁)
(((L9 `) + x) `) + ((((L9 `) + y) `) + x) is M2( the U1 of c₁)
x + L9 is M2( the U1 of c₁)
(((L9 `) + y) `) + L9 is M2( the U1 of c₁)
x + ((((L9 `) + y) `) + L9) is M2( the U1 of c₁)
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
(x `) ` is M2( the U1 of c<sub>1</sub>)
L9 + ((x `) `) is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(x `) + L9 is M2( the U1 of c₁)
((x `) + L9) ` is M2( the U1 of c₁)
(((x `) + L9) `) + L9 is M2( the U1 of c₁)
(((x `) + L9) `) + ((((x `) + L9) `) + L9) is M2( the U1 of c₁)
((x `) `) ` is M2( the U1 of c<sub>1</sub>)
(((x `) `) `) + L9 is M2( the U1 of c₁)
((((x `) `) `) + L9) ` is M2( the U1 of c₁)
(((((x `) `) `) + L9) `) + L9 is M2( the U1 of c₁)
(((x `) + L9) `) + ((((((x `) `) `) + L9) `) + L9) is M2( the U1 of c₁)
(((((x `) `) `) + L9) `) + ((((((x `) `) `) + L9) `) + L9) is M2( the U1 of c₁)
L9 is M2( the U1 of c₁)
L9 ` is M2( the U1 of c<sub>1</sub>)
(L9 `) ` is M2( the U1 of c<sub>1</sub>)
((L9 `) `) ` is M2( the U1 of c₁)
(((L9 `) `) `) + ((L9 `) `) is M2( the U1 of c<sub>1</sub>)
((((L9 `) `) `) + ((L9 `) `)) ` is M2( the U1 of c<sub>1</sub>)
(((((L9 `) `) `) + ((L9 `) `)) `) + ((L9 `) `) is M2( the U1 of c<sub>1</sub>)
(L9 `) + ((L9 `) `) is M2( the U1 of c₁)
((L9 `) + ((L9 `) `)) ` is M2( the U1 of c₁)
(((L9 `) + ((L9 `) `)) `) + ((L9 `) `) is M2( the U1 of c₁)
(((L9 `) + ((L9 `) `)) `) + L9 is M2( the U1 of c₁)
L9 is M2( the U1 of c₁)
L9 ` is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
x + L9 is M2( the U1 of c<sub>1</sub>)
(x + L9) ` is M2( the U1 of c₁)
y is M2( the U1 of c₁)
((x + L9) `) + y is M2( the U1 of c<sub>1</sub>)
(((x + L9) `) + y) ` is M2( the U1 of c<sub>1</sub>)
(L9 `) + ((((x + L9) `) + y) `) is M2( the U1 of c₁)
((L9 `) + ((((x + L9) `) + y) `)) ` is M2( the U1 of c₁)
x + ((((x + L9) `) + y) `) is M2( the U1 of c₁)
(((L9 `) + ((((x + L9) `) + y) `)) `) + (x + ((((x + L9) `) + y) `)) is M2( the U1 of c₁)
((((x + L9) `) + y) `) + (x + L9) is M2( the U1 of c₁)
L9 is M2( the U1 of c₁)
L9 ` is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
(L9 `) + ((L9 + x) `) is M2( the U1 of c₁)
((L9 `) + ((L9 + x) `)) ` is M2( the U1 of c<sub>1</sub>)
x ` is M2( the U1 of c₁)
(x `) + ((L9 + x) `) is M2( the U1 of c₁)
(((L9 `) + ((L9 + x) `)) `) + ((x `) + ((L9 + x) `)) is M2( the U1 of c<sub>1</sub>)
(x `) + L9 is M2( the U1 of c₁)
((x `) + L9) ` is M2( the U1 of c₁)
(((x `) + L9) `) + L9 is M2( the U1 of c₁)
((((x `) + L9) `) + L9) ` is M2( the U1 of c<sub>1</sub>)
(x `) + (((((x `) + L9) `) + L9) `) is M2( the U1 of c<sub>1</sub>)
(((L9 `) + ((L9 + x) `)) `) + ((x `) + (((((x `) + L9) `) + L9) `)) is M2( the U1 of c₁)
(L9 `) + (((((x `) + L9) `) + L9) `) is M2( the U1 of c₁)
((L9 `) + (((((x `) + L9) `) + L9) `)) ` is M2( the U1 of c<sub>1</sub>)
(((L9 `) + (((((x `) + L9) `) + L9) `)) `) + ((x `) + (((((x `) + L9) `) + L9) `)) is M2( the U1 of c₁)
L9 is M2( the U1 of c₁)
L9 ` is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
(L9 `) + x is M2( the U1 of c₁)
((L9 `) + x) ` is M2( the U1 of c₁)
L9 + (((L9 `) + x) `) is M2( the U1 of c₁)
(((L9 `) + x) `) + L9 is M2( the U1 of c₁)
((((L9 `) + x) `) + L9) + (((L9 `) + x) `) is M2( the U1 of c₁)
L9 is M2( the U1 of c₁)
L9 ` is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
(L9 `) + ((L9 + x) `) is M2( the U1 of c₁)
(L9 `) ` is M2( the U1 of c₁)
((L9 `) `) + x is M2( the U1 of c₁)
(((L9 `) `) + x) ` is M2( the U1 of c<sub>1</sub>)
(L9 `) + ((((L9 `) `) + x) `) is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
x + (L9 `) is M2( the U1 of c<sub>1</sub>)
(x + (L9 `)) ` is M2( the U1 of c<sub>1</sub>)
L9 + ((x + (L9 `)) `) is M2( the U1 of c<sub>1</sub>)
((x + (L9 `)) `) + L9 is M2( the U1 of c<sub>1</sub>)
(((x + (L9 `)) `) + L9) + ((x + (L9 `)) `) is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
x is M2( the U1 of c₁)
x + L9 is M2( the U1 of c₁)
(x + L9) ` is M2( the U1 of c<sub>1</sub>)
(L9 `) + ((x + L9) `) is M2( the U1 of c<sub>1</sub>)
(L9 `) ` is M2( the U1 of c<sub>1</sub>)
x + ((L9 `) `) is M2( the U1 of c<sub>1</sub>)
(x + ((L9 `) `)) ` is M2( the U1 of c₁)
(L9 `) + ((x + ((L9 `) `)) `) is M2( the U1 of c₁)
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
L9 + (x `) is M2( the U1 of c₁)
(x `) + L9 is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
L9 + x is M2( the U1 of c₁)
(L9 + x) ` is M2( the U1 of c<sub>1</sub>)
(L9 `) + ((L9 + x) `) is M2( the U1 of c<sub>1</sub>)
((L9 `) + ((L9 + x) `)) ` is M2( the U1 of c₁)
(x `) + ((L9 + x) `) is M2( the U1 of c₁)
(((L9 `) + ((L9 + x) `)) `) + ((x `) + ((L9 + x) `)) is M2( the U1 of c<sub>1</sub>)
(L9 `) ` is M2( the U1 of c<sub>1</sub>)
((L9 `) `) + ((x `) + ((L9 + x) `)) is M2( the U1 of c<sub>1</sub>)
((L9 `) `) + (x `) is M2( the U1 of c₁)
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
L9 + x is M2( the U1 of c₁)
x + L9 is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
(x `) ` is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
x is M2( the U1 of c₁)
(L9 `) + x is M2( the U1 of c<sub>1</sub>)
((L9 `) + x) ` is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
(((L9 `) + x) `) + y is M2( the U1 of c<sub>1</sub>)
((((L9 `) + x) `) + y) ` is M2( the U1 of c₁)
(L9 `) + y is M2( the U1 of c<sub>1</sub>)
(((((L9 `) + x) `) + y) `) + ((L9 `) + y) is M2( the U1 of c<sub>1</sub>)
y + ((L9 `) + x) is M2( the U1 of c₁)
(L9 `) + ((L9 `) + x) is M2( the U1 of c₁)
y + ((L9 `) + ((L9 `) + x)) is M2( the U1 of c₁)
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
(x `) + L9 is M2( the U1 of c₁)
L9 + ((x `) + L9) is M2( the U1 of c<sub>1</sub>)
((x `) + L9) ` is M2( the U1 of c<sub>1</sub>)
(((x `) + L9) `) + L9 is M2( the U1 of c<sub>1</sub>)
((((x `) + L9) `) + L9) ` is M2( the U1 of c₁)
(((((x `) + L9) `) + L9) `) + ((x `) + L9) is M2( the U1 of c₁)
L9 is M2( the U1 of c₁)
x is M2( the U1 of c₁)
L9 + x is M2( the U1 of c₁)
(L9 + x) ` is M2( the U1 of c<sub>1</sub>)
((L9 + x) `) + L9 is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
(x `) + L9 is M2( the U1 of c₁)
L9 + ((x `) + L9) is M2( the U1 of c<sub>1</sub>)
((x `) + L9) ` is M2( the U1 of c<sub>1</sub>)
(((x `) + L9) `) + L9 is M2( the U1 of c<sub>1</sub>)
((((x `) + L9) `) + L9) ` is M2( the U1 of c₁)
(((((x `) + L9) `) + L9) `) + L9 is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
(L9 + x) ` is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
(x `) + L9 is M2( the U1 of c₁)
((x `) + L9) ` is M2( the U1 of c₁)
((L9 + x) `) + (((x `) + L9) `) is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
(L9 `) + (((x `) + L9) `) is M2( the U1 of c<sub>1</sub>)
(((x `) + L9) `) + L9 is M2( the U1 of c<sub>1</sub>)
((((x `) + L9) `) + L9) ` is M2( the U1 of c₁)
(((((x `) + L9) `) + L9) `) + (((x `) + L9) `) is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
L9 ` is M2( the U1 of c₁)
x is M2( the U1 of c₁)
x ` is M2( the U1 of c<sub>1</sub>)
(L9 `) + (x `) is M2( the U1 of c<sub>1</sub>)
((L9 `) + (x `)) ` is M2( the U1 of c₁)
(L9 `) + x is M2( the U1 of c<sub>1</sub>)
((L9 `) + x) ` is M2( the U1 of c<sub>1</sub>)
(((L9 `) + (x `)) `) + (((L9 `) + x) `) is M2( the U1 of c₁)
(x `) + (L9 `) is M2( the U1 of c₁)
((x `) + (L9 `)) ` is M2( the U1 of c<sub>1</sub>)
(((x `) + (L9 `)) `) + (((L9 `) + x) `) is M2( the U1 of c₁)
(((L9 `) + x) `) + (((x `) + (L9 `)) `) is M2( the U1 of c<sub>1</sub>)
(L9 `) ` is M2( the U1 of c<sub>1</sub>)
((L9 `) `) + (((x `) + (L9 `)) `) is M2( the U1 of c₁)
L9 + (((x `) + (L9 `)) `) is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
x + y is M2( the U1 of c<sub>1</sub>)
(L9 + x) + (x + y) is M2( the U1 of c<sub>1</sub>)
(L9 + x) + y is M2( the U1 of c<sub>1</sub>)
y ` is M2( the U1 of c₁)
(y `) + (L9 + x) is M2( the U1 of c<sub>1</sub>)
((y `) + (L9 + x)) ` is M2( the U1 of c<sub>1</sub>)
(((y `) + (L9 + x)) `) + (L9 + x) is M2( the U1 of c<sub>1</sub>)
x + (L9 + x) is M2( the U1 of c<sub>1</sub>)
(((y `) + (L9 + x)) `) + (x + (L9 + x)) is M2( the U1 of c<sub>1</sub>)
L9 is M2( the U1 of c<sub>1</sub>)
x is M2( the U1 of c<sub>1</sub>)
L9 + x is M2( the U1 of c<sub>1</sub>)
y is M2( the U1 of c<sub>1</sub>)
(L9 + x) + y is M2( the U1 of c<sub>1</sub>)
x + y is M2( the U1 of c<sub>1</sub>)
L9 + (x + y) is M2( the U1 of c<sub>1</sub>)
z is M2( the U1 of c<sub>1</sub>)
Z is M2( the U1 of c<sub>1</sub>)
z + Z is M2( the U1 of c<sub>1</sub>)
z is M2( the U1 of c<sub>1</sub>)
z + z is M2( the U1 of c<sub>1</sub>)
(z + Z) + (z + z) is M2( the U1 of c<sub>1</sub>)
z + z is M2( the U1 of c<sub>1</sub>)
Z + (z + z) is M2( the U1 of c<sub>1</sub>)
(z + z) + (z + Z) is M2( the U1 of c<sub>1</sub>)
(z + z) + Z is M2( the U1 of c<sub>1</sub>)
(z + z) + Z is M2( the U1 of c<sub>1</sub>)
x + L9 is M2( the U1 of c<sub>1</sub>)
y + x is M2( the U1 of c<sub>1</sub>)
(x + L9) + (y + x) is M2( the U1 of c<sub>1</sub>)
(L9 + x) + (y + x) is M2( the U1 of c<sub>1</sub>)
(L9 + x) + (x + y) is M2( the U1 of c<sub>1</sub>)
c<sub>1</sub> is non empty ComplLLattStr
c<sub>1</sub> is non empty ComplLLattStr
L9 is non empty join-commutative join-associative upper-bounded Huntington join-idempotent ComplLLattStr
the U1 of L9 is V11() set
x is M2( the U1 of L9)
x ` is M2( the U1 of L9)
y is M2( the U1 of L9)
(x `) + y is M2( the U1 of L9)
((x `) + y) ` is M2( the U1 of L9)
z is M2( the U1 of L9)
z + y is M2( the U1 of L9)
(((x `) + y) `) + (z + y) is M2( the U1 of L9)
z + x is M2( the U1 of L9)
y + (z + x) is M2( the U1 of L9)
z + y is M2( the U1 of L9)
y ` is M2( the U1 of L9)
(z + y) + (y `) is M2( the U1 of L9)
y + (y `) is M2( the U1 of L9)
z + (y + (y `)) is M2( the U1 of L9)
Top L9 is M2( the U1 of L9)
z + (Top L9) is M2( the U1 of L9)
(x `) + y is M2( the U1 of L9)
((x `) + y) ` is M2( the U1 of L9)
(((x `) + y) `) + (z + y) is M2( the U1 of L9)
(y `) ` is M2( the U1 of L9)
(x `) + ((y `) `) is M2( the U1 of L9)
((x `) + ((y `) `)) ` is M2( the U1 of L9)
(((x `) + ((y `) `)) `) + (z + y) is M2( the U1 of L9)
x *' (y `) is M2( the U1 of L9)
(x *' (y `)) + (z + y) is M2( the U1 of L9)
(z + y) + x is M2( the U1 of L9)
((z + y) + x) *' ((z + y) + (y `)) is M2( the U1 of L9)
z + x is M2( the U1 of L9)
y + (z + x) is M2( the U1 of L9)
the U1 of L9 is V11() set
x is M2( the U1 of L9)
x ` is M2( the U1 of L9)
y is M2( the U1 of L9)
(x `) + y is M2( the U1 of L9)
((x `) + y) ` is M2( the U1 of L9)
(((x `) + y) `) + x is M2( the U1 of L9)
(x `) + y is M2( the U1 of L9)
((x `) + y) ` is M2( the U1 of L9)
(((x `) + y) `) + x is M2( the U1 of L9)
y ` is M2( the U1 of L9)
(y `) ` is M2( the U1 of L9)
(x `) + ((y `) `) is M2( the U1 of L9)
((x `) + ((y `) `)) ` is M2( the U1 of L9)
(((x `) + ((y `) `)) `) + x is M2( the U1 of L9)
x *' (y `) is M2( the U1 of L9)
(x *' (y `)) + x is M2( the U1 of L9)
c₁ is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like OrthoLattStr
c₁ is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like well-complemented OrthoLattStr