:: SHEFFER1 semantic presentation

K92() is V26() V31() cardinal limit_cardinal set
K19(K92()) is V31() set
1 is set
K20(1,1) is set
K19(K20(1,1)) is set
K20(K20(1,1),1) is set
K19(K20(K20(1,1),1)) is set
{} is set
{{}} is non empty V12() 1 -element set
L is non empty join-commutative join-associative upper-bounded Huntington join-idempotent ComplLLattStr
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
b + a is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . (b,a) is M2( the carrier of L)
(b + a) ` is M2( the carrier of L)
the Compl of L is V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))
K19(K20( the carrier of L, the carrier of L)) is set
K72( the carrier of L, the carrier of L, the Compl of L,(b + a)) is M2( the carrier of L)
b ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,b) is M2( the carrier of L)
a ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,a) is M2( the carrier of L)
(b `) *' (a `) is M2( the carrier of L)
(b `) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,(b `)) is M2( the carrier of L)
(a `) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,(a `)) is M2( the carrier of L)
((b `) `) "\/" ((a `) `) is M2( the carrier of L)
the L_join of L . (((b `) `),((a `) `)) is M2( the carrier of L)
(((b `) `) "\/" ((a `) `)) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,(((b `) `) "\/" ((a `) `))) is M2( the carrier of L)
((b `) *' (a `)) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,((b `) *' (a `))) is M2( the carrier of L)
L is non empty LattStr
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
a "/\" b is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . (a,b) is M2( the carrier of L)
L is non empty LattStr
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
a "\/" b is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . (a,b) is M2( the carrier of L)
L is non empty LattStr
the carrier of L is non empty set
L is non empty LattStr
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
X is M2( the carrier of L)
(L) is M2( the carrier of L)
X "/\" (L) is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . (X,(L)) is M2( the carrier of L)
b "\/" a is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_join of L . (b,a) is M2( the carrier of L)
X "/\" (b "\/" a) is M2( the carrier of L)
the L_meet of L . (X,(b "\/" a)) is M2( the carrier of L)
X "/\" b is M2( the carrier of L)
the L_meet of L . (X,b) is M2( the carrier of L)
X "/\" a is M2( the carrier of L)
the L_meet of L . (X,a) is M2( the carrier of L)
(X "/\" b) "\/" (X "/\" a) is M2( the carrier of L)
the L_join of L . ((X "/\" b),(X "/\" a)) is M2( the carrier of L)
b "/\" X is M2( the carrier of L)
the L_meet of L . (b,X) is M2( the carrier of L)
(b "/\" X) "\/" (X "/\" a) is M2( the carrier of L)
the L_join of L . ((b "/\" X),(X "/\" a)) is M2( the carrier of L)
a "/\" X is M2( the carrier of L)
the L_meet of L . (a,X) is M2( the carrier of L)
(b "/\" X) "\/" (a "/\" X) is M2( the carrier of L)
the L_join of L . ((b "/\" X),(a "/\" X)) is M2( the carrier of L)
(L) is M2( the carrier of L)
(L) "\/" (a "/\" X) is M2( the carrier of L)
the L_join of L . ((L),(a "/\" X)) is M2( the carrier of L)
a "/\" b is M2( the carrier of L)
the L_meet of L . (a,b) is M2( the carrier of L)
(a "/\" b) "\/" (a "/\" X) is M2( the carrier of L)
the L_join of L . ((a "/\" b),(a "/\" X)) is M2( the carrier of L)
b "\/" X is M2( the carrier of L)
the L_join of L . (b,X) is M2( the carrier of L)
a "/\" (b "\/" X) is M2( the carrier of L)
the L_meet of L . (a,(b "\/" X)) is M2( the carrier of L)
a "/\" (L) is M2( the carrier of L)
the L_meet of L . (a,(L)) is M2( the carrier of L)
the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is non empty V12() V31() 1 -element set
the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
a is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) "/\" a is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_meet of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is V6() V18(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) M2(K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )))
K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is set
K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is set
K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )) is set
the L_meet of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . ( the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ),a) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
X is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
X "/\" the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_meet of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . (X, the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is non empty V12() V31() 1 -element set
the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
a is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) "\/" a is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is V6() V18(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) M2(K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )))
K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is set
K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is set
K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )) is set
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . ( the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ),a) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
X is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
X "\/" the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . (X, the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is non empty V12() V31() 1 -element set
b is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
a is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
b "\/" a is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is V6() V18(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) M2(K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )))
K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is set
K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is set
K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )) is set
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . (b,a) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
Top the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
b "/\" a is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_meet of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is V6() V18(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) M2(K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )))
the L_meet of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . (b,a) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
Bottom the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
b is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
b "\/" b is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is V6() V18(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) M2(K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )))
K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is set
K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is set
K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )) is set
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . (b,b) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
b is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
a is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
b "\/" a is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is V6() V18(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) M2(K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )))
K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is set
K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is set
K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )) is set
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . (b,a) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
( the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
b "/\" a is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_meet of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is V6() V18(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) M2(K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )))
the L_meet of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . (b,a) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
( the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
b is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
a is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
X is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
a "\/" X is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is V6() V18(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) M2(K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )))
K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is set
K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is set
K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )) is set
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . (a,X) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
b "/\" (a "\/" X) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_meet of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is V6() V18(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) M2(K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )))
the L_meet of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . (b,(a "\/" X)) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
b "/\" a is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_meet of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . (b,a) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
b "/\" X is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_meet of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . (b,X) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
(b "/\" a) "\/" (b "/\" X) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . ((b "/\" a),(b "/\" X)) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
a is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) "\/" a is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is V6() V18(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) M2(K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )))
K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is set
K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is set
K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )) is set
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . ( the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ),a) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
X is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
X "\/" the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . (X, the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
a is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) "/\" a is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_meet of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is V6() V18(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) M2(K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )))
K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is set
K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is set
K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )) is set
the L_meet of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . ( the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ),a) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
X is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
X "/\" the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_meet of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . (X, the M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
b is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
a is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
X is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
a "/\" X is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_meet of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is V6() V18(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) M2(K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )))
K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is set
K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) is set
K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )) is set
the L_meet of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . (a,X) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
b "\/" (a "/\" X) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr is V6() V18(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ) M2(K19(K20(K20( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr , the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ), the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )))
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . (b,(a "/\" X)) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
b "\/" a is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . (b,a) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
b "\/" X is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_join of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . (b,X) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
(b "\/" a) "/\" (b "\/" X) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
the L_meet of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr . ((b "\/" a),(b "\/" X)) is M2( the carrier of the non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr )
L is non empty join-commutative meet-commutative distributive () () () LattStr
the carrier of L is non empty set
(L) is M2( the carrier of L)
b is M2( the carrier of L)
(L,b) is M2( the carrier of L)
b "\/" (L,b) is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . (b,(L,b)) is M2( the carrier of L)
L is non empty join-commutative meet-commutative distributive () () () LattStr
the carrier of L is non empty set
(L) is M2( the carrier of L)
b is M2( the carrier of L)
(L,b) is M2( the carrier of L)
b "/\" (L,b) is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . (b,(L,b)) is M2( the carrier of L)
L is non empty join-commutative meet-commutative distributive join-idempotent () () () LattStr
the carrier of L is non empty set
(L) is M2( the carrier of L)
b is M2( the carrier of L)
b "\/" (L) is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . (b,(L)) is M2( the carrier of L)
(b "\/" (L)) "/\" (L) is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_meet of L . ((b "\/" (L)),(L)) is M2( the carrier of L)
(L,b) is M2( the carrier of L)
b "\/" (L,b) is M2( the carrier of L)
the L_join of L . (b,(L,b)) is M2( the carrier of L)
(b "\/" (L)) "/\" (b "\/" (L,b)) is M2( the carrier of L)
the L_meet of L . ((b "\/" (L)),(b "\/" (L,b))) is M2( the carrier of L)
(L) "/\" (L,b) is M2( the carrier of L)
the L_meet of L . ((L),(L,b)) is M2( the carrier of L)
b "\/" ((L) "/\" (L,b)) is M2( the carrier of L)
the L_join of L . (b,((L) "/\" (L,b))) is M2( the carrier of L)
L is non empty join-commutative meet-commutative distributive join-idempotent () () () () LattStr
the carrier of L is non empty set
(L) is M2( the carrier of L)
b is M2( the carrier of L)
b "/\" (L) is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . (b,(L)) is M2( the carrier of L)
(b "/\" (L)) "\/" (L) is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_join of L . ((b "/\" (L)),(L)) is M2( the carrier of L)
(L,b) is M2( the carrier of L)
b "/\" (L,b) is M2( the carrier of L)
the L_meet of L . (b,(L,b)) is M2( the carrier of L)
(b "/\" (L)) "\/" (b "/\" (L,b)) is M2( the carrier of L)
the L_join of L . ((b "/\" (L)),(b "/\" (L,b))) is M2( the carrier of L)
(L) "\/" (L,b) is M2( the carrier of L)
the L_join of L . ((L),(L,b)) is M2( the carrier of L)
b "/\" ((L) "\/" (L,b)) is M2( the carrier of L)
the L_meet of L . (b,((L) "\/" (L,b))) is M2( the carrier of L)
L is non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent LattStr
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
b "\/" a is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . (b,a) is M2( the carrier of L)
X is M2( the carrier of L)
(b "\/" a) "\/" X is M2( the carrier of L)
the L_join of L . ((b "\/" a),X) is M2( the carrier of L)
((b "\/" a) "\/" X) "/\" b is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_meet of L . (((b "\/" a) "\/" X),b) is M2( the carrier of L)
b "/\" (b "\/" a) is M2( the carrier of L)
the L_meet of L . (b,(b "\/" a)) is M2( the carrier of L)
b "/\" X is M2( the carrier of L)
the L_meet of L . (b,X) is M2( the carrier of L)
(b "/\" (b "\/" a)) "\/" (b "/\" X) is M2( the carrier of L)
the L_join of L . ((b "/\" (b "\/" a)),(b "/\" X)) is M2( the carrier of L)
b "/\" b is M2( the carrier of L)
the L_meet of L . (b,b) is M2( the carrier of L)
b "/\" a is M2( the carrier of L)
the L_meet of L . (b,a) is M2( the carrier of L)
(b "/\" b) "\/" (b "/\" a) is M2( the carrier of L)
the L_join of L . ((b "/\" b),(b "/\" a)) is M2( the carrier of L)
((b "/\" b) "\/" (b "/\" a)) "\/" (b "/\" X) is M2( the carrier of L)
the L_join of L . (((b "/\" b) "\/" (b "/\" a)),(b "/\" X)) is M2( the carrier of L)
b "\/" (b "/\" a) is M2( the carrier of L)
the L_join of L . (b,(b "/\" a)) is M2( the carrier of L)
(b "\/" (b "/\" a)) "\/" (b "/\" X) is M2( the carrier of L)
the L_join of L . ((b "\/" (b "/\" a)),(b "/\" X)) is M2( the carrier of L)
b "\/" (b "/\" X) is M2( the carrier of L)
the L_join of L . (b,(b "/\" X)) is M2( the carrier of L)
L is non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent () LattStr
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
b "/\" a is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . (b,a) is M2( the carrier of L)
X is M2( the carrier of L)
(b "/\" a) "/\" X is M2( the carrier of L)
the L_meet of L . ((b "/\" a),X) is M2( the carrier of L)
((b "/\" a) "/\" X) "\/" b is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_join of L . (((b "/\" a) "/\" X),b) is M2( the carrier of L)
b "\/" (b "/\" a) is M2( the carrier of L)
the L_join of L . (b,(b "/\" a)) is M2( the carrier of L)
b "\/" X is M2( the carrier of L)
the L_join of L . (b,X) is M2( the carrier of L)
(b "\/" (b "/\" a)) "/\" (b "\/" X) is M2( the carrier of L)
the L_meet of L . ((b "\/" (b "/\" a)),(b "\/" X)) is M2( the carrier of L)
b "\/" b is M2( the carrier of L)
the L_join of L . (b,b) is M2( the carrier of L)
b "\/" a is M2( the carrier of L)
the L_join of L . (b,a) is M2( the carrier of L)
(b "\/" b) "/\" (b "\/" a) is M2( the carrier of L)
the L_meet of L . ((b "\/" b),(b "\/" a)) is M2( the carrier of L)
((b "\/" b) "/\" (b "\/" a)) "/\" (b "\/" X) is M2( the carrier of L)
the L_meet of L . (((b "\/" b) "/\" (b "\/" a)),(b "\/" X)) is M2( the carrier of L)
b "/\" (b "\/" a) is M2( the carrier of L)
the L_meet of L . (b,(b "\/" a)) is M2( the carrier of L)
(b "/\" (b "\/" a)) "/\" (b "\/" X) is M2( the carrier of L)
the L_meet of L . ((b "/\" (b "\/" a)),(b "\/" X)) is M2( the carrier of L)
b "/\" (b "\/" X) is M2( the carrier of L)
the L_meet of L . (b,(b "\/" X)) is M2( the carrier of L)
L is non empty join-commutative meet-commutative distributive () () () () LattStr
the carrier of L is non empty set
b is M2( the carrier of L)
b "/\" b is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . (b,b) is M2( the carrier of L)
(L) is M2( the carrier of L)
(b "/\" b) "\/" (L) is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_join of L . ((b "/\" b),(L)) is M2( the carrier of L)
(L,b) is M2( the carrier of L)
b "/\" (L,b) is M2( the carrier of L)
the L_meet of L . (b,(L,b)) is M2( the carrier of L)
(b "/\" b) "\/" (b "/\" (L,b)) is M2( the carrier of L)
the L_join of L . ((b "/\" b),(b "/\" (L,b))) is M2( the carrier of L)
b "\/" (L,b) is M2( the carrier of L)
the L_join of L . (b,(L,b)) is M2( the carrier of L)
b "/\" (b "\/" (L,b)) is M2( the carrier of L)
the L_meet of L . (b,(b "\/" (L,b))) is M2( the carrier of L)
(L) is M2( the carrier of L)
b "/\" (L) is M2( the carrier of L)
the L_meet of L . (b,(L)) is M2( the carrier of L)
L is non empty join-commutative meet-commutative distributive () () () () LattStr
the carrier of L is non empty set
b is M2( the carrier of L)
b "\/" b is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . (b,b) is M2( the carrier of L)
b "\/" b is M2( the carrier of L)
(L) is M2( the carrier of L)
(b "\/" b) "/\" (L) is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_meet of L . ((b "\/" b),(L)) is M2( the carrier of L)
(L,b) is M2( the carrier of L)
b "\/" (L,b) is M2( the carrier of L)
the L_join of L . (b,(L,b)) is M2( the carrier of L)
(b "\/" b) "/\" (b "\/" (L,b)) is M2( the carrier of L)
the L_meet of L . ((b "\/" b),(b "\/" (L,b))) is M2( the carrier of L)
b "/\" (L,b) is M2( the carrier of L)
the L_meet of L . (b,(L,b)) is M2( the carrier of L)
b "\/" (b "/\" (L,b)) is M2( the carrier of L)
the L_join of L . (b,(b "/\" (L,b))) is M2( the carrier of L)
(L) is M2( the carrier of L)
b "\/" (L) is M2( the carrier of L)
the L_join of L . (b,(L)) is M2( the carrier of L)
L is non empty join-commutative meet-commutative distributive join-idempotent () () () LattStr
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
b "/\" a is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . (b,a) is M2( the carrier of L)
(b "/\" a) "\/" a is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_join of L . ((b "/\" a),a) is M2( the carrier of L)
a "/\" b is M2( the carrier of L)
the L_meet of L . (a,b) is M2( the carrier of L)
a "\/" (a "/\" b) is M2( the carrier of L)
the L_join of L . (a,(a "/\" b)) is M2( the carrier of L)
(L) is M2( the carrier of L)
(L) "/\" a is M2( the carrier of L)
the L_meet of L . ((L),a) is M2( the carrier of L)
((L) "/\" a) "\/" (a "/\" b) is M2( the carrier of L)
the L_join of L . (((L) "/\" a),(a "/\" b)) is M2( the carrier of L)
(L) "\/" b is M2( the carrier of L)
the L_join of L . ((L),b) is M2( the carrier of L)
a "/\" ((L) "\/" b) is M2( the carrier of L)
the L_meet of L . (a,((L) "\/" b)) is M2( the carrier of L)
a "/\" (L) is M2( the carrier of L)
the L_meet of L . (a,(L)) is M2( the carrier of L)
L is non empty join-commutative meet-commutative distributive join-idempotent () () () () LattStr
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
b "\/" a is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . (b,a) is M2( the carrier of L)
b "/\" (b "\/" a) is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_meet of L . (b,(b "\/" a)) is M2( the carrier of L)
b "\/" a is M2( the carrier of L)
b "/\" (b "\/" a) is M2( the carrier of L)
the L_meet of L . (b,(b "\/" a)) is M2( the carrier of L)
b "/\" b is M2( the carrier of L)
the L_meet of L . (b,b) is M2( the carrier of L)
b "/\" a is M2( the carrier of L)
the L_meet of L . (b,a) is M2( the carrier of L)
(b "/\" b) "\/" (b "/\" a) is M2( the carrier of L)
the L_join of L . ((b "/\" b),(b "/\" a)) is M2( the carrier of L)
b "\/" (b "/\" a) is M2( the carrier of L)
the L_join of L . (b,(b "/\" a)) is M2( the carrier of L)
L is non empty join-commutative meet-commutative distributive join-idempotent () () () () LattStr
the carrier of L is non empty set
(L) is M2( the carrier of L)
b is M2( the carrier of L)
(L) "\/" b is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . ((L),b) is M2( the carrier of L)
b "\/" (L) is M2( the carrier of L)
the L_join of L . (b,(L)) is M2( the carrier of L)
b is M2( the carrier 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 V68() complemented Boolean LattStr
the carrier of L is non empty set
Top L is M2( the carrier of L)
b is M2( the carrier of L)
a is M2( the carrier of L)
b "/\" a is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . (b,a) is M2( the carrier of L)
a "/\" b is M2( the carrier of L)
the L_meet of L . (a,b) is M2( the carrier of L)
b is M2( the carrier of L)
L is non empty join-commutative meet-commutative distributive join-idempotent () () () () LattStr
the carrier of L is non empty set
(L) is M2( the carrier of L)
b is M2( the carrier of L)
(L) "/\" b is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . ((L),b) is M2( the carrier of L)
b "/\" (L) is M2( the carrier of L)
the L_meet of L . (b,(L)) is M2( the carrier of L)
b is M2( the carrier 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 V68() complemented Boolean LattStr
the carrier of L is non empty set
Bottom L is M2( the carrier of L)
b is M2( the carrier of L)
a is M2( the carrier of L)
b "\/" a is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . (b,a) is M2( the carrier of L)
a "\/" b is M2( the carrier of L)
the L_join of L . (a,b) is M2( the carrier of L)
b is M2( the carrier of L)
L is non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent LattStr
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
X is M2( the carrier of L)
a "\/" X is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . (a,X) is M2( the carrier of L)
b "\/" (a "\/" X) is M2( the carrier of L)
the L_join of L . (b,(a "\/" X)) is M2( the carrier of L)
b "\/" a is M2( the carrier of L)
the L_join of L . (b,a) is M2( the carrier of L)
(b "\/" a) "\/" X is M2( the carrier of L)
the L_join of L . ((b "\/" a),X) is M2( the carrier of L)
a "\/" X is M2( the carrier of L)
(a "\/" X) "\/" b is M2( the carrier of L)
the L_join of L . ((a "\/" X),b) is M2( the carrier of L)
((a "\/" X) "\/" b) "/\" a is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_meet of L . (((a "\/" X) "\/" b),a) is M2( the carrier of L)
a "/\" (a "\/" X) is M2( the carrier of L)
the L_meet of L . (a,(a "\/" X)) is M2( the carrier of L)
a "/\" b is M2( the carrier of L)
the L_meet of L . (a,b) is M2( the carrier of L)
(a "/\" (a "\/" X)) "\/" (a "/\" b) is M2( the carrier of L)
the L_join of L . ((a "/\" (a "\/" X)),(a "/\" b)) is M2( the carrier of L)
a "/\" a is M2( the carrier of L)
the L_meet of L . (a,a) is M2( the carrier of L)
a "/\" X is M2( the carrier of L)
the L_meet of L . (a,X) is M2( the carrier of L)
(a "/\" a) "\/" (a "/\" X) is M2( the carrier of L)
the L_join of L . ((a "/\" a),(a "/\" X)) is M2( the carrier of L)
((a "/\" a) "\/" (a "/\" X)) "\/" (a "/\" b) is M2( the carrier of L)
the L_join of L . (((a "/\" a) "\/" (a "/\" X)),(a "/\" b)) is M2( the carrier of L)
a "\/" (a "/\" X) is M2( the carrier of L)
the L_join of L . (a,(a "/\" X)) is M2( the carrier of L)
(a "\/" (a "/\" X)) "\/" (a "/\" b) is M2( the carrier of L)
the L_join of L . ((a "\/" (a "/\" X)),(a "/\" b)) is M2( the carrier of L)
a "\/" (a "/\" b) is M2( the carrier of L)
the L_join of L . (a,(a "/\" b)) is M2( the carrier of L)
b "\/" a is M2( the carrier of L)
(b "\/" a) "\/" X is M2( the carrier of L)
the L_join of L . ((b "\/" a),X) is M2( the carrier of L)
((b "\/" a) "\/" X) "/\" b is M2( the carrier of L)
the L_meet of L . (((b "\/" a) "\/" X),b) is M2( the carrier of L)
b "\/" (a "\/" X) is M2( the carrier of L)
the L_join of L . (b,(a "\/" X)) is M2( the carrier of L)
((b "\/" a) "\/" X) "/\" (b "\/" (a "\/" X)) is M2( the carrier of L)
the L_meet of L . (((b "\/" a) "\/" X),(b "\/" (a "\/" X))) is M2( the carrier of L)
(b "\/" a) "/\" (b "\/" (a "\/" X)) is M2( the carrier of L)
the L_meet of L . ((b "\/" a),(b "\/" (a "\/" X))) is M2( the carrier of L)
X "/\" (b "\/" (a "\/" X)) is M2( the carrier of L)
the L_meet of L . (X,(b "\/" (a "\/" X))) is M2( the carrier of L)
((b "\/" a) "/\" (b "\/" (a "\/" X))) "\/" (X "/\" (b "\/" (a "\/" X))) is M2( the carrier of L)
the L_join of L . (((b "\/" a) "/\" (b "\/" (a "\/" X))),(X "/\" (b "\/" (a "\/" X)))) is M2( the carrier of L)
((b "\/" a) "/\" (b "\/" (a "\/" X))) "\/" X is M2( the carrier of L)
the L_join of L . (((b "\/" a) "/\" (b "\/" (a "\/" X))),X) is M2( the carrier of L)
b "/\" (b "\/" (a "\/" X)) is M2( the carrier of L)
the L_meet of L . (b,(b "\/" (a "\/" X))) is M2( the carrier of L)
a "/\" (b "\/" (a "\/" X)) is M2( the carrier of L)
the L_meet of L . (a,(b "\/" (a "\/" X))) is M2( the carrier of L)
(b "/\" (b "\/" (a "\/" X))) "\/" (a "/\" (b "\/" (a "\/" X))) is M2( the carrier of L)
the L_join of L . ((b "/\" (b "\/" (a "\/" X))),(a "/\" (b "\/" (a "\/" X)))) is M2( the carrier of L)
((b "/\" (b "\/" (a "\/" X))) "\/" (a "/\" (b "\/" (a "\/" X)))) "\/" X is M2( the carrier of L)
the L_join of L . (((b "/\" (b "\/" (a "\/" X))) "\/" (a "/\" (b "\/" (a "\/" X)))),X) is M2( the carrier of L)
((b "\/" a) "\/" X) "/\" (a "\/" X) is M2( the carrier of L)
the L_meet of L . (((b "\/" a) "\/" X),(a "\/" X)) is M2( the carrier of L)
(((b "\/" a) "\/" X) "/\" b) "\/" (((b "\/" a) "\/" X) "/\" (a "\/" X)) is M2( the carrier of L)
the L_join of L . ((((b "\/" a) "\/" X) "/\" b),(((b "\/" a) "\/" X) "/\" (a "\/" X))) is M2( the carrier of L)
((b "\/" a) "\/" X) "/\" a is M2( the carrier of L)
the L_meet of L . (((b "\/" a) "\/" X),a) is M2( the carrier of L)
((b "\/" a) "\/" X) "/\" X is M2( the carrier of L)
the L_meet of L . (((b "\/" a) "\/" X),X) is M2( the carrier of L)
(((b "\/" a) "\/" X) "/\" a) "\/" (((b "\/" a) "\/" X) "/\" X) is M2( the carrier of L)
the L_join of L . ((((b "\/" a) "\/" X) "/\" a),(((b "\/" a) "\/" X) "/\" X)) is M2( the carrier of L)
b "\/" ((((b "\/" a) "\/" X) "/\" a) "\/" (((b "\/" a) "\/" X) "/\" X)) is M2( the carrier of L)
the L_join of L . (b,((((b "\/" a) "\/" X) "/\" a) "\/" (((b "\/" a) "\/" X) "/\" X))) is M2( the carrier of L)
a "\/" (((b "\/" a) "\/" X) "/\" X) is M2( the carrier of L)
the L_join of L . (a,(((b "\/" a) "\/" X) "/\" X)) is M2( the carrier of L)
b "\/" (a "\/" (((b "\/" a) "\/" X) "/\" X)) is M2( the carrier of L)
the L_join of L . (b,(a "\/" (((b "\/" a) "\/" X) "/\" X))) is M2( the carrier of L)
(b "\/" a) "/\" X is M2( the carrier of L)
the L_meet of L . ((b "\/" a),X) is M2( the carrier of L)
X "/\" X is M2( the carrier of L)
the L_meet of L . (X,X) is M2( the carrier of L)
((b "\/" a) "/\" X) "\/" (X "/\" X) is M2( the carrier of L)
the L_join of L . (((b "\/" a) "/\" X),(X "/\" X)) is M2( the carrier of L)
a "\/" (((b "\/" a) "/\" X) "\/" (X "/\" X)) is M2( the carrier of L)
the L_join of L . (a,(((b "\/" a) "/\" X) "\/" (X "/\" X))) is M2( the carrier of L)
b "\/" (a "\/" (((b "\/" a) "/\" X) "\/" (X "/\" X))) is M2( the carrier of L)
the L_join of L . (b,(a "\/" (((b "\/" a) "/\" X) "\/" (X "/\" X)))) is M2( the carrier of L)
((b "\/" a) "/\" X) "\/" X is M2( the carrier of L)
the L_join of L . (((b "\/" a) "/\" X),X) is M2( the carrier of L)
a "\/" (((b "\/" a) "/\" X) "\/" X) is M2( the carrier of L)
the L_join of L . (a,(((b "\/" a) "/\" X) "\/" X)) is M2( the carrier of L)
b "\/" (a "\/" (((b "\/" a) "/\" X) "\/" X)) is M2( the carrier of L)
the L_join of L . (b,(a "\/" (((b "\/" a) "/\" X) "\/" X))) is M2( the carrier of L)
L is non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent () LattStr
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
X is M2( the carrier of L)
a "/\" X is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . (a,X) is M2( the carrier of L)
b "/\" (a "/\" X) is M2( the carrier of L)
the L_meet of L . (b,(a "/\" X)) is M2( the carrier of L)
b "/\" a is M2( the carrier of L)
the L_meet of L . (b,a) is M2( the carrier of L)
(b "/\" a) "/\" X is M2( the carrier of L)
the L_meet of L . ((b "/\" a),X) is M2( the carrier of L)
b "/\" a is M2( the carrier of L)
(b "/\" a) "/\" X is M2( the carrier of L)
the L_meet of L . ((b "/\" a),X) is M2( the carrier of L)
((b "/\" a) "/\" X) "\/" b is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_join of L . (((b "/\" a) "/\" X),b) is M2( the carrier of L)
a "/\" X is M2( the carrier of L)
(a "/\" X) "/\" b is M2( the carrier of L)
the L_meet of L . ((a "/\" X),b) is M2( the carrier of L)
((a "/\" X) "/\" b) "\/" a is M2( the carrier of L)
the L_join of L . (((a "/\" X) "/\" b),a) is M2( the carrier of L)
a "\/" (a "/\" X) is M2( the carrier of L)
the L_join of L . (a,(a "/\" X)) is M2( the carrier of L)
a "\/" b is M2( the carrier of L)
the L_join of L . (a,b) is M2( the carrier of L)
(a "\/" (a "/\" X)) "/\" (a "\/" b) is M2( the carrier of L)
the L_meet of L . ((a "\/" (a "/\" X)),(a "\/" b)) is M2( the carrier of L)
a "\/" a is M2( the carrier of L)
the L_join of L . (a,a) is M2( the carrier of L)
a "\/" X is M2( the carrier of L)
the L_join of L . (a,X) is M2( the carrier of L)
(a "\/" a) "/\" (a "\/" X) is M2( the carrier of L)
the L_meet of L . ((a "\/" a),(a "\/" X)) is M2( the carrier of L)
((a "\/" a) "/\" (a "\/" X)) "/\" (a "\/" b) is M2( the carrier of L)
the L_meet of L . (((a "\/" a) "/\" (a "\/" X)),(a "\/" b)) is M2( the carrier of L)
a "/\" (a "\/" X) is M2( the carrier of L)
the L_meet of L . (a,(a "\/" X)) is M2( the carrier of L)
(a "/\" (a "\/" X)) "/\" (a "\/" b) is M2( the carrier of L)
the L_meet of L . ((a "/\" (a "\/" X)),(a "\/" b)) is M2( the carrier of L)
a "/\" (a "\/" b) is M2( the carrier of L)
the L_meet of L . (a,(a "\/" b)) is M2( the carrier of L)
b "/\" (a "/\" X) is M2( the carrier of L)
the L_meet of L . (b,(a "/\" X)) is M2( the carrier of L)
((b "/\" a) "/\" X) "\/" (b "/\" (a "/\" X)) is M2( the carrier of L)
the L_join of L . (((b "/\" a) "/\" X),(b "/\" (a "/\" X))) is M2( the carrier of L)
(b "/\" a) "\/" (b "/\" (a "/\" X)) is M2( the carrier of L)
the L_join of L . ((b "/\" a),(b "/\" (a "/\" X))) is M2( the carrier of L)
X "\/" (b "/\" (a "/\" X)) is M2( the carrier of L)
the L_join of L . (X,(b "/\" (a "/\" X))) is M2( the carrier of L)
((b "/\" a) "\/" (b "/\" (a "/\" X))) "/\" (X "\/" (b "/\" (a "/\" X))) is M2( the carrier of L)
the L_meet of L . (((b "/\" a) "\/" (b "/\" (a "/\" X))),(X "\/" (b "/\" (a "/\" X)))) is M2( the carrier of L)
((b "/\" a) "\/" (b "/\" (a "/\" X))) "/\" X is M2( the carrier of L)
the L_meet of L . (((b "/\" a) "\/" (b "/\" (a "/\" X))),X) is M2( the carrier of L)
b "\/" (b "/\" (a "/\" X)) is M2( the carrier of L)
the L_join of L . (b,(b "/\" (a "/\" X))) is M2( the carrier of L)
a "\/" (b "/\" (a "/\" X)) is M2( the carrier of L)
the L_join of L . (a,(b "/\" (a "/\" X))) is M2( the carrier of L)
(b "\/" (b "/\" (a "/\" X))) "/\" (a "\/" (b "/\" (a "/\" X))) is M2( the carrier of L)
the L_meet of L . ((b "\/" (b "/\" (a "/\" X))),(a "\/" (b "/\" (a "/\" X)))) is M2( the carrier of L)
((b "\/" (b "/\" (a "/\" X))) "/\" (a "\/" (b "/\" (a "/\" X)))) "/\" X is M2( the carrier of L)
the L_meet of L . (((b "\/" (b "/\" (a "/\" X))) "/\" (a "\/" (b "/\" (a "/\" X)))),X) is M2( the carrier of L)
((b "/\" a) "/\" X) "\/" (a "/\" X) is M2( the carrier of L)
the L_join of L . (((b "/\" a) "/\" X),(a "/\" X)) is M2( the carrier of L)
(((b "/\" a) "/\" X) "\/" b) "/\" (((b "/\" a) "/\" X) "\/" (a "/\" X)) is M2( the carrier of L)
the L_meet of L . ((((b "/\" a) "/\" X) "\/" b),(((b "/\" a) "/\" X) "\/" (a "/\" X))) is M2( the carrier of L)
((b "/\" a) "/\" X) "\/" a is M2( the carrier of L)
the L_join of L . (((b "/\" a) "/\" X),a) is M2( the carrier of L)
((b "/\" a) "/\" X) "\/" X is M2( the carrier of L)
the L_join of L . (((b "/\" a) "/\" X),X) is M2( the carrier of L)
(((b "/\" a) "/\" X) "\/" a) "/\" (((b "/\" a) "/\" X) "\/" X) is M2( the carrier of L)
the L_meet of L . ((((b "/\" a) "/\" X) "\/" a),(((b "/\" a) "/\" X) "\/" X)) is M2( the carrier of L)
b "/\" ((((b "/\" a) "/\" X) "\/" a) "/\" (((b "/\" a) "/\" X) "\/" X)) is M2( the carrier of L)
the L_meet of L . (b,((((b "/\" a) "/\" X) "\/" a) "/\" (((b "/\" a) "/\" X) "\/" X))) is M2( the carrier of L)
a "/\" (((b "/\" a) "/\" X) "\/" X) is M2( the carrier of L)
the L_meet of L . (a,(((b "/\" a) "/\" X) "\/" X)) is M2( the carrier of L)
b "/\" (a "/\" (((b "/\" a) "/\" X) "\/" X)) is M2( the carrier of L)
the L_meet of L . (b,(a "/\" (((b "/\" a) "/\" X) "\/" X))) is M2( the carrier of L)
(b "/\" a) "\/" X is M2( the carrier of L)
the L_join of L . ((b "/\" a),X) is M2( the carrier of L)
X "\/" X is M2( the carrier of L)
the L_join of L . (X,X) is M2( the carrier of L)
((b "/\" a) "\/" X) "/\" (X "\/" X) is M2( the carrier of L)
the L_meet of L . (((b "/\" a) "\/" X),(X "\/" X)) is M2( the carrier of L)
a "/\" (((b "/\" a) "\/" X) "/\" (X "\/" X)) is M2( the carrier of L)
the L_meet of L . (a,(((b "/\" a) "\/" X) "/\" (X "\/" X))) is M2( the carrier of L)
b "/\" (a "/\" (((b "/\" a) "\/" X) "/\" (X "\/" X))) is M2( the carrier of L)
the L_meet of L . (b,(a "/\" (((b "/\" a) "\/" X) "/\" (X "\/" X)))) is M2( the carrier of L)
((b "/\" a) "\/" X) "/\" X is M2( the carrier of L)
the L_meet of L . (((b "/\" a) "\/" X),X) is M2( the carrier of L)
a "/\" (((b "/\" a) "\/" X) "/\" X) is M2( the carrier of L)
the L_meet of L . (a,(((b "/\" a) "\/" X) "/\" X)) is M2( the carrier of L)
b "/\" (a "/\" (((b "/\" a) "\/" X) "/\" X)) is M2( the carrier of L)
the L_meet of L . (b,(a "/\" (((b "/\" a) "\/" X) "/\" X))) is M2( the carrier of L)
L is non empty join-commutative meet-commutative distributive join-idempotent () () () () LattStr
Top L is M2( the carrier of L)
the carrier of L is non empty set
(L) is M2( the carrier of L)
a is M2( the carrier of L)
(L) "\/" a is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . ((L),a) is M2( the carrier of L)
X is M2( the carrier of L)
X "\/" (L) is M2( the carrier of L)
the L_join of L . (X,(L)) is M2( the carrier of L)
L is non empty join-commutative meet-commutative distributive join-idempotent () () () () LattStr
Bottom L is M2( the carrier of L)
the carrier of L is non empty set
(L) is M2( the carrier of L)
a is M2( the carrier of L)
(L) "/\" a is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . ((L),a) is M2( the carrier of L)
X is M2( the carrier of L)
X "/\" (L) is M2( the carrier of L)
the L_meet of L . (X,(L)) is M2( the carrier 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 V68() complemented Boolean () LattStr
Top L is M2( the carrier of L)
the carrier of L is non empty set
(L) is M2( the carrier of L)
a is M2( the carrier of L)
(Top L) "/\" a is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . ((Top L),a) is M2( the carrier of L)
X is M2( the carrier of L)
X "/\" (Top L) is M2( the carrier of L)
the L_meet of L . (X,(Top L)) is M2( the carrier 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 V68() complemented Boolean () LattStr
Bottom L is M2( the carrier of L)
the carrier of L is non empty set
(L) is M2( the carrier of L)
a is M2( the carrier of L)
(Bottom L) "\/" a is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . ((Bottom L),a) is M2( the carrier of L)
X is M2( the carrier of L)
X "\/" (Bottom L) is M2( the carrier of L)
the L_join of L . (X,(Bottom L)) is M2( the carrier of L)
L is non empty join-commutative meet-commutative distributive join-idempotent () () () () LattStr
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
b "/\" a is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . (b,a) is M2( the carrier of L)
(L) is M2( the carrier of L)
Bottom L is M2( the carrier of L)
b "\/" a is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_join of L . (b,a) is M2( the carrier of L)
(L) is M2( the carrier of L)
Top L is M2( the carrier of L)
L is non empty join-commutative meet-commutative distributive join-idempotent () () () () LattStr
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
b "/\" a is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . (b,a) is M2( the carrier of L)
(L) is M2( the carrier of L)
Bottom L is M2( the carrier of L)
b "\/" a is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_join of L . (b,a) is M2( the carrier of L)
(L) is M2( the carrier of L)
Top L is M2( the carrier 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 V68() complemented Boolean () () () LattStr
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
b "/\" a is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . (b,a) is M2( the carrier of L)
Bottom L is M2( the carrier of L)
(L) is M2( the carrier of L)
b "\/" a is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_join of L . (b,a) is M2( the carrier of L)
Top L is M2( the carrier of L)
(L) is M2( the carrier of L)
L is non empty LattStr
b is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean LattStr
the carrier of b is non empty set
Bottom b is M2( the carrier of b)
a is M2( the carrier of b)
(Bottom b) "\/" a is M2( the carrier of b)
the L_join of b is V6() V18(K20( the carrier of b, the carrier of b), the carrier of b) M2(K19(K20(K20( the carrier of b, the carrier of b), the carrier of b)))
K20( the carrier of b, the carrier of b) is set
K20(K20( the carrier of b, the carrier of b), the carrier of b) is set
K19(K20(K20( the carrier of b, the carrier of b), the carrier of b)) is set
the L_join of b . ((Bottom b),a) is M2( the carrier of b)
X is M2( the carrier of b)
X "\/" (Bottom b) is M2( the carrier of b)
the L_join of b . (X,(Bottom b)) is M2( the carrier of b)
a is M2( the carrier of b)
Top b is M2( the carrier of b)
a is M2( the carrier of b)
(Top b) "/\" a is M2( the carrier of b)
the L_meet of b is V6() V18(K20( the carrier of b, the carrier of b), the carrier of b) M2(K19(K20(K20( the carrier of b, the carrier of b), the carrier of b)))
K20( the carrier of b, the carrier of b) is set
K20(K20( the carrier of b, the carrier of b), the carrier of b) is set
K19(K20(K20( the carrier of b, the carrier of b), the carrier of b)) is set
the L_meet of b . ((Top b),a) is M2( the carrier of b)
X is M2( the carrier of b)
X "/\" (Top b) is M2( the carrier of b)
the L_meet of b . (X,(Top b)) is M2( the carrier of b)
a is M2( the carrier of b)
a is M2( the carrier of b)
X is M2( the carrier of b)
a is M2( the carrier of b)
X "\/" a is M2( the carrier of b)
the L_join of b is V6() V18(K20( the carrier of b, the carrier of b), the carrier of b) M2(K19(K20(K20( the carrier of b, the carrier of b), the carrier of b)))
K20( the carrier of b, the carrier of b) is set
K20(K20( the carrier of b, the carrier of b), the carrier of b) is set
K19(K20(K20( the carrier of b, the carrier of b), the carrier of b)) is set
the L_join of b . (X,a) is M2( the carrier of b)
a "/\" (X "\/" a) is M2( the carrier of b)
the L_meet of b is V6() V18(K20( the carrier of b, the carrier of b), the carrier of b) M2(K19(K20(K20( the carrier of b, the carrier of b), the carrier of b)))
the L_meet of b . (a,(X "\/" a)) is M2( the carrier of b)
a "/\" X is M2( the carrier of b)
the L_meet of b . (a,X) is M2( the carrier of b)
a "/\" a is M2( the carrier of b)
the L_meet of b . (a,a) is M2( the carrier of b)
(a "/\" X) "\/" (a "/\" a) is M2( the carrier of b)
the L_join of b . ((a "/\" X),(a "/\" a)) is M2( the carrier of b)
a is M2( the carrier of b)
X is M2( the carrier of b)
a is M2( the carrier of b)
X "/\" a is M2( the carrier of b)
the L_meet of b is V6() V18(K20( the carrier of b, the carrier of b), the carrier of b) M2(K19(K20(K20( the carrier of b, the carrier of b), the carrier of b)))
K20( the carrier of b, the carrier of b) is set
K20(K20( the carrier of b, the carrier of b), the carrier of b) is set
K19(K20(K20( the carrier of b, the carrier of b), the carrier of b)) is set
the L_meet of b . (X,a) is M2( the carrier of b)
a "\/" (X "/\" a) is M2( the carrier of b)
the L_join of b is V6() V18(K20( the carrier of b, the carrier of b), the carrier of b) M2(K19(K20(K20( the carrier of b, the carrier of b), the carrier of b)))
the L_join of b . (a,(X "/\" a)) is M2( the carrier of b)
a "\/" X is M2( the carrier of b)
the L_join of b . (a,X) is M2( the carrier of b)
a "\/" a is M2( the carrier of b)
the L_join of b . (a,a) is M2( the carrier of b)
(a "\/" X) "/\" (a "\/" a) is M2( the carrier of b)
the L_meet of b . ((a "\/" X),(a "\/" a)) is M2( the carrier of b)
b is non empty join-commutative meet-commutative distributive join-idempotent () () () () LattStr
L is non empty LattStr
L is non empty LattStr
op2 is V6() V18(K20(1,1),1) M2(K19(K20(K20(1,1),1)))
op1 is V6() V18(1,1) M2(K19(K20(1,1)))
(1,op2,op2,op1,op2) is () ()
() is ()
K20({{}},{{}}) is set
K20(K20({{}},{{}}),{{}}) is set
K19(K20(K20({{}},{{}}),{{}})) is set
the V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}}))) is V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}})))
({{}}, the V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}})))) is () ()
the carrier of ({{}}, the V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}})))) is set
K20({{}},{{}}) is set
K20(K20({{}},{{}}),{{}}) is set
K19(K20(K20({{}},{{}}),{{}})) is set
the V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}}))) is V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}})))
({{}}, the V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}}))), the V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}}))), the V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}})))) is () ()
the carrier of ({{}}, the V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}}))), the V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}}))), the V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}})))) is set
K20({{}},{{}}) is set
K20(K20({{}},{{}}),{{}}) is set
K19(K20(K20({{}},{{}}),{{}})) is set
the V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}}))) is V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}})))
K19(K20({{}},{{}})) is set
the V6() V18({{}},{{}}) M2(K19(K20({{}},{{}}))) is V6() V18({{}},{{}}) M2(K19(K20({{}},{{}})))
({{}}, the V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}}))), the V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}}))), the V6() V18({{}},{{}}) M2(K19(K20({{}},{{}}))), the V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}})))) is () ()
the carrier of ({{}}, the V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}}))), the V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}}))), the V6() V18({{}},{{}}) M2(K19(K20({{}},{{}}))), the V6() V18(K20({{}},{{}}),{{}}) M2(K19(K20(K20({{}},{{}}),{{}})))) is set
L is non empty ()
the carrier of L is non empty set
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
b is M2( the carrier of L)
a is M2( the carrier of L)
the of L . (b,a) is M2( the carrier of L)
L is non empty V45() V46() 1 -element ()
the carrier of L is non empty V12() V31() 1 -element set
b is M2( the carrier of L)
(L,b,b) is M2( the carrier of L)
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the of L . (b,b) is M2( the carrier of L)
(L,(L,b,b),(L,b,b)) is M2( the carrier of L)
the of L . ((L,b,b),(L,b,b)) is M2( the carrier of L)
the carrier of L is non empty V12() V31() 1 -element set
b is M2( the carrier of L)
a is M2( the carrier of L)
(L,a,a) is M2( the carrier of L)
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the of L . (a,a) is M2( the carrier of L)
(L,a,(L,a,a)) is M2( the carrier of L)
the of L . (a,(L,a,a)) is M2( the carrier of L)
(L,b,(L,a,(L,a,a))) is M2( the carrier of L)
the of L . (b,(L,a,(L,a,a))) is M2( the carrier of L)
(L,b,b) is M2( the carrier of L)
the of L . (b,b) is M2( the carrier of L)
the carrier of L is non empty V12() V31() 1 -element set
b is M2( the carrier of L)
a is M2( the carrier of L)
X is M2( the carrier of L)
(L,a,X) is M2( the carrier of L)
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the of L . (a,X) is M2( the carrier of L)
(L,b,(L,a,X)) is M2( the carrier of L)
the of L . (b,(L,a,X)) is M2( the carrier of L)
(L,(L,b,(L,a,X)),(L,b,(L,a,X))) is M2( the carrier of L)
the of L . ((L,b,(L,a,X)),(L,b,(L,a,X))) is M2( the carrier of L)
(L,a,a) is M2( the carrier of L)
the of L . (a,a) is M2( the carrier of L)
(L,(L,a,a),b) is M2( the carrier of L)
the of L . ((L,a,a),b) is M2( the carrier of L)
(L,X,X) is M2( the carrier of L)
the of L . (X,X) is M2( the carrier of L)
(L,(L,X,X),b) is M2( the carrier of L)
the of L . ((L,X,X),b) is M2( the carrier of L)
(L,(L,(L,a,a),b),(L,(L,X,X),b)) is M2( the carrier of L)
the of L . ((L,(L,a,a),b),(L,(L,X,X),b)) is M2( the carrier of L)
L is non empty V45() V46() 1 -element \/-SemiLattStr
the carrier of L is non empty V12() V31() 1 -element set
b is M2( the carrier of L)
a is M2( the carrier of L)
b "\/" a is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . (b,a) is M2( the carrier of L)
a "\/" b is M2( the carrier of L)
the L_join of L . (a,b) is M2( the carrier of L)
the carrier of L is non empty V12() V31() 1 -element set
b is M2( the carrier of L)
a is M2( the carrier of L)
X is M2( the carrier of L)
a "\/" X is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . (a,X) is M2( the carrier of L)
b "\/" (a "\/" X) is M2( the carrier of L)
the L_join of L . (b,(a "\/" X)) is M2( the carrier of L)
b "\/" a is M2( the carrier of L)
the L_join of L . (b,a) is M2( the carrier of L)
(b "\/" a) "\/" X is M2( the carrier of L)
the L_join of L . ((b "\/" a),X) is M2( the carrier of L)
L is non empty V45() V46() 1 -element /\-SemiLattStr
the carrier of L is non empty V12() V31() 1 -element set
b is M2( the carrier of L)
a is M2( the carrier of L)
b "/\" a is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . (b,a) is M2( the carrier of L)
a "/\" b is M2( the carrier of L)
the L_meet of L . (a,b) is M2( the carrier of L)
the carrier of L is non empty V12() V31() 1 -element set
b is M2( the carrier of L)
a is M2( the carrier of L)
X is M2( the carrier of L)
a "/\" X is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . (a,X) is M2( the carrier of L)
b "/\" (a "/\" X) is M2( the carrier of L)
the L_meet of L . (b,(a "/\" X)) is M2( the carrier of L)
b "/\" a is M2( the carrier of L)
the L_meet of L . (b,a) is M2( the carrier of L)
(b "/\" a) "/\" X is M2( the carrier of L)
the L_meet of L . ((b "/\" a),X) is M2( the carrier of L)
L is non empty V45() V46() 1 -element join-commutative join-associative meet-commutative meet-associative LattStr
the carrier of L is non empty V12() V31() 1 -element set
b is M2( the carrier of L)
a is M2( the carrier of L)
b "\/" a is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . (b,a) is M2( the carrier of L)
b "/\" (b "\/" a) is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_meet of L . (b,(b "\/" a)) is M2( the carrier of L)
the carrier of L is non empty V12() V31() 1 -element set
the M2( the carrier of L) is M2( the carrier of L)
a is M2( the carrier of L)
the M2( the carrier of L) "\/" a is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . ( the M2( the carrier of L),a) is M2( the carrier of L)
a "\/" the M2( the carrier of L) is M2( the carrier of L)
the L_join of L . (a, the M2( the carrier of L)) is M2( the carrier of L)
the carrier of L is non empty V12() V31() 1 -element set
b is M2( the carrier of L)
a is M2( the carrier of L)
b "/\" a is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . (b,a) is M2( the carrier of L)
(b "/\" a) "\/" a is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_join of L . ((b "/\" a),a) is M2( the carrier of L)
the carrier of L is non empty V12() V31() 1 -element set
the M2( the carrier of L) is M2( the carrier of L)
a is M2( the carrier of L)
the M2( the carrier of L) "/\" a is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . ( the M2( the carrier of L),a) is M2( the carrier of L)
a "/\" the M2( the carrier of L) is M2( the carrier of L)
the L_meet of L . (a, the M2( the carrier of L)) is M2( the carrier of L)
the carrier of L is non empty V12() V31() 1 -element set
the M2( the carrier of L) is M2( the carrier of L)
a is M2( the carrier of L)
the M2( the carrier of L) "/\" a is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . ( the M2( the carrier of L),a) is M2( the carrier of L)
Bottom L is M2( the carrier of L)
a "/\" the M2( the carrier of L) is M2( the carrier of L)
the L_meet of L . (a, the M2( the carrier of L)) is M2( the carrier of L)
the M2( the carrier of L) "\/" a is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_join of L . ( the M2( the carrier of L),a) is M2( the carrier of L)
Top L is M2( the carrier of L)
a "\/" the M2( the carrier of L) is M2( the carrier of L)
the L_join of L . (a, the M2( the carrier of L)) is M2( the carrier of L)
the carrier of L is non empty V12() V31() 1 -element set
b is M2( the carrier of L)
a is M2( the carrier of L)
X is M2( the carrier of L)
a "\/" X is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . (a,X) is M2( the carrier of L)
b "/\" (a "\/" X) is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_meet of L . (b,(a "\/" X)) is M2( the carrier of L)
b "/\" a is M2( the carrier of L)
the L_meet of L . (b,a) is M2( the carrier of L)
b "/\" X is M2( the carrier of L)
the L_meet of L . (b,X) is M2( the carrier of L)
(b "/\" a) "\/" (b "/\" X) is M2( the carrier of L)
the L_join of L . ((b "/\" a),(b "/\" X)) is M2( the carrier of L)
the carrier of () is non empty V12() V31() 1 -element set
b is M2( the carrier of ())
a is M2( the carrier of ())
b "/\" a is M2( the carrier of ())
the L_meet of () is V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))
K20( the carrier of (), the carrier of ()) is set
K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is set
K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is set
the L_meet of () . (b,a) is M2( the carrier of ())
((),b,a) is M2( the carrier of ())
the of () is V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))
the of () . (b,a) is M2( the carrier of ())
((),((),b,a),((),b,a)) is M2( the carrier of ())
the of () . (((),b,a),((),b,a)) is M2( the carrier of ())
X is M2( the carrier of ())
a is M2( the carrier of ())
((),X,a) is M2( the carrier of ())
the of () . (X,a) is M2( the carrier of ())
X ` is M2( the carrier of ())
the Compl of () is V6() V18( the carrier of (), the carrier of ()) M2(K19(K20( the carrier of (), the carrier of ())))
K19(K20( the carrier of (), the carrier of ())) is set
K72( the carrier of (), the carrier of (), the Compl of (),X) is M2( the carrier of ())
a ` is M2( the carrier of ())
K72( the carrier of (), the carrier of (), the Compl of (),a) is M2( the carrier of ())
(X `) + (a `) is M2( the carrier of ())
the L_join of () is V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))
the L_join of () . ((X `),(a `)) is M2( the carrier of ())
b is M2( the carrier of ())
((),b,b) is M2( the carrier of ())
the of () is V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))
K20( the carrier of (), the carrier of ()) is set
K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is set
K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is set
the of () . (b,b) is M2( the carrier of ())
b ` is M2( the carrier of ())
the Compl of () is V6() V18( the carrier of (), the carrier of ()) M2(K19(K20( the carrier of (), the carrier of ())))
K19(K20( the carrier of (), the carrier of ())) is set
K72( the carrier of (), the carrier of (), the Compl of (),b) is M2( the carrier of ())
a is M2( the carrier of ())
X is M2( the carrier of ())
a "\/" X is M2( the carrier of ())
the L_join of () is V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))
the L_join of () . (a,X) is M2( the carrier of ())
((),a,a) is M2( the carrier of ())
the of () . (a,a) is M2( the carrier of ())
((),X,X) is M2( the carrier of ())
the of () . (X,X) is M2( the carrier of ())
((),((),a,a),((),X,X)) is M2( the carrier of ())
the of () . (((),a,a),((),X,X)) is M2( the carrier of ())
b is M2( the carrier of ())
b ` is M2( the carrier of ())
the Compl of () is V6() V18( the carrier of (), the carrier of ()) M2(K19(K20( the carrier of (), the carrier of ())))
K20( the carrier of (), the carrier of ()) is set
K19(K20( the carrier of (), the carrier of ())) is set
K72( the carrier of (), the carrier of (), the Compl of (),b) is M2( the carrier of ())
b "\/" (b `) is M2( the carrier of ())
the L_join of () is V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))
K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is set
K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is set
the L_join of () . (b,(b `)) is M2( the carrier of ())
Top () is M2( the carrier of ())
b "/\" (b `) is M2( the carrier of ())
the L_meet of () is V6() V18(K20( the carrier of (), the carrier of ()), the carrier of ()) M2(K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())))
the L_meet of () . (b,(b `)) is M2( the carrier of ())
Bottom () is M2( the carrier of ())
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean Robbins Huntington join-idempotent well-complemented () () () () () ()
the carrier of L is non empty set
b is M2( the carrier of L)
(L,b,b) is M2( the carrier of L)
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the of L . (b,b) is M2( the carrier of L)
(L,(L,b,b),(L,b,b)) is M2( the carrier of L)
the of L . ((L,b,b),(L,b,b)) is M2( the carrier of L)
b ` is M2( the carrier of L)
the Compl of L is V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))
K19(K20( the carrier of L, the carrier of L)) is set
K72( the carrier of L, the carrier of L, the Compl of L,b) is M2( the carrier of L)
(b `) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,(b `)) is M2( the carrier of L)
(L,b,b) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,(L,b,b)) is M2( the carrier 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 V68() complemented Boolean Robbins Huntington join-idempotent well-complemented () () () () () ()
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
(L,a,a) is M2( the carrier of L)
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the of L . (a,a) is M2( the carrier of L)
(L,a,(L,a,a)) is M2( the carrier of L)
the of L . (a,(L,a,a)) is M2( the carrier of L)
(L,b,(L,a,(L,a,a))) is M2( the carrier of L)
the of L . (b,(L,a,(L,a,a))) is M2( the carrier of L)
(L,b,b) is M2( the carrier of L)
the of L . (b,b) is M2( the carrier of L)
b ` is M2( the carrier of L)
the Compl of L is V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))
K19(K20( the carrier of L, the carrier of L)) is set
K72( the carrier of L, the carrier of L, the Compl of L,b) is M2( the carrier of L)
Bot L is M2( the carrier of L)
(b `) + (Bot L) is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_join of L . ((b `),(Bot L)) is M2( the carrier of L)
a ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,a) is M2( the carrier of L)
(a `) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,(a `)) is M2( the carrier of L)
((a `) `) *' (a `) is M2( the carrier of L)
((a `) `) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,((a `) `)) is M2( the carrier of L)
(((a `) `) `) "\/" ((a `) `) is M2( the carrier of L)
the L_join of L . ((((a `) `) `),((a `) `)) is M2( the carrier of L)
((((a `) `) `) "\/" ((a `) `)) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,((((a `) `) `) "\/" ((a `) `))) is M2( the carrier of L)
(b `) + (((a `) `) *' (a `)) is M2( the carrier of L)
the L_join of L . ((b `),(((a `) `) *' (a `))) is M2( the carrier of L)
(a `) + a is M2( the carrier of L)
the L_join of L . ((a `),a) is M2( the carrier of L)
((a `) + a) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,((a `) + a)) is M2( the carrier of L)
(b `) + (((a `) + a) `) is M2( the carrier of L)
the L_join of L . ((b `),(((a `) + a) `)) is M2( the carrier of L)
(L,b,((a `) + a)) is M2( the carrier of L)
the of L . (b,((a `) + a)) is M2( the carrier of L)
(a `) + ((a `) `) is M2( the carrier of L)
the L_join of L . ((a `),((a `) `)) is M2( the carrier of L)
(L,b,((a `) + ((a `) `))) is M2( the carrier of L)
the of L . (b,((a `) + ((a `) `))) is M2( the carrier of L)
(L,a,(a `)) is M2( the carrier of L)
the of L . (a,(a `)) is M2( the carrier of L)
(L,b,(L,a,(a `))) is M2( the carrier of L)
the of L . (b,(L,a,(a `))) is M2( the carrier 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 V68() complemented Boolean Robbins Huntington join-idempotent well-complemented () () () () () ()
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
X is M2( the carrier of L)
(L,a,X) is M2( the carrier of L)
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the of L . (a,X) is M2( the carrier of L)
(L,b,(L,a,X)) is M2( the carrier of L)
the of L . (b,(L,a,X)) is M2( the carrier of L)
(L,(L,b,(L,a,X)),(L,b,(L,a,X))) is M2( the carrier of L)
the of L . ((L,b,(L,a,X)),(L,b,(L,a,X))) is M2( the carrier of L)
(L,a,a) is M2( the carrier of L)
the of L . (a,a) is M2( the carrier of L)
(L,(L,a,a),b) is M2( the carrier of L)
the of L . ((L,a,a),b) is M2( the carrier of L)
(L,X,X) is M2( the carrier of L)
the of L . (X,X) is M2( the carrier of L)
(L,(L,X,X),b) is M2( the carrier of L)
the of L . ((L,X,X),b) is M2( the carrier of L)
(L,(L,(L,a,a),b),(L,(L,X,X),b)) is M2( the carrier of L)
the of L . ((L,(L,a,a),b),(L,(L,X,X),b)) is M2( the carrier of L)
a ` is M2( the carrier of L)
the Compl of L is V6() V18( the carrier of L, the carrier of L) M2(K19(K20( the carrier of L, the carrier of L)))
K19(K20( the carrier of L, the carrier of L)) is set
K72( the carrier of L, the carrier of L, the Compl of L,a) is M2( the carrier of L)
X ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,X) is M2( the carrier of L)
(a `) + (X `) is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_join of L . ((a `),(X `)) is M2( the carrier of L)
b *' ((a `) + (X `)) is M2( the carrier of L)
b ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,b) is M2( the carrier of L)
((a `) + (X `)) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,((a `) + (X `))) is M2( the carrier of L)
(b `) "\/" (((a `) + (X `)) `) is M2( the carrier of L)
the L_join of L . ((b `),(((a `) + (X `)) `)) is M2( the carrier of L)
((b `) "\/" (((a `) + (X `)) `)) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,((b `) "\/" (((a `) + (X `)) `))) is M2( the carrier of L)
(a `) *' b is M2( the carrier of L)
(a `) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,(a `)) is M2( the carrier of L)
((a `) `) "\/" (b `) is M2( the carrier of L)
the L_join of L . (((a `) `),(b `)) is M2( the carrier of L)
(((a `) `) "\/" (b `)) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,(((a `) `) "\/" (b `))) is M2( the carrier of L)
(X `) *' b is M2( the carrier of L)
(X `) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,(X `)) is M2( the carrier of L)
((X `) `) "\/" (b `) is M2( the carrier of L)
the L_join of L . (((X `) `),(b `)) is M2( the carrier of L)
(((X `) `) "\/" (b `)) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,(((X `) `) "\/" (b `))) is M2( the carrier of L)
((a `) *' b) + ((X `) *' b) is M2( the carrier of L)
the L_join of L . (((a `) *' b),((X `) *' b)) is M2( the carrier of L)
(L,a,X) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,(L,a,X)) is M2( the carrier of L)
(b `) + ((L,a,X) `) is M2( the carrier of L)
the L_join of L . ((b `),((L,a,X) `)) is M2( the carrier of L)
((b `) + ((L,a,X) `)) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,((b `) + ((L,a,X) `))) is M2( the carrier of L)
(L,b,(L,a,X)) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,(L,b,(L,a,X))) is M2( the carrier of L)
(b `) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,(b `)) is M2( the carrier of L)
(a `) *' ((b `) `) is M2( the carrier of L)
((b `) `) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,((b `) `)) is M2( the carrier of L)
((a `) `) "\/" (((b `) `) `) is M2( the carrier of L)
the L_join of L . (((a `) `),(((b `) `) `)) is M2( the carrier of L)
(((a `) `) "\/" (((b `) `) `)) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,(((a `) `) "\/" (((b `) `) `))) is M2( the carrier of L)
((a `) *' ((b `) `)) + ((X `) *' b) is M2( the carrier of L)
the L_join of L . (((a `) *' ((b `) `)),((X `) *' b)) is M2( the carrier of L)
(X `) *' ((b `) `) is M2( the carrier of L)
((X `) `) "\/" (((b `) `) `) is M2( the carrier of L)
the L_join of L . (((X `) `),(((b `) `) `)) is M2( the carrier of L)
(((X `) `) "\/" (((b `) `) `)) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,(((X `) `) "\/" (((b `) `) `))) is M2( the carrier of L)
((a `) *' ((b `) `)) + ((X `) *' ((b `) `)) is M2( the carrier of L)
the L_join of L . (((a `) *' ((b `) `)),((X `) *' ((b `) `))) is M2( the carrier of L)
a + (b `) is M2( the carrier of L)
the L_join of L . (a,(b `)) is M2( the carrier of L)
(a + (b `)) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,(a + (b `))) is M2( the carrier of L)
((a + (b `)) `) + ((X `) *' ((b `) `)) is M2( the carrier of L)
the L_join of L . (((a + (b `)) `),((X `) *' ((b `) `))) is M2( the carrier of L)
X + (b `) is M2( the carrier of L)
the L_join of L . (X,(b `)) is M2( the carrier of L)
(X + (b `)) ` is M2( the carrier of L)
K72( the carrier of L, the carrier of L, the Compl of L,(X + (b `))) is M2( the carrier of L)
((a + (b `)) `) + ((X + (b `)) `) is M2( the carrier of L)
the L_join of L . (((a + (b `)) `),((X + (b `)) `)) is M2( the carrier of L)
(L,(a + (b `)),(X + (b `))) is M2( the carrier of L)
the of L . ((a + (b `)),(X + (b `))) is M2( the carrier of L)
((a `) `) + (b `) is M2( the carrier of L)
(L,(((a `) `) + (b `)),(X + (b `))) is M2( the carrier of L)
the of L . ((((a `) `) + (b `)),(X + (b `))) is M2( the carrier of L)
((X `) `) + (b `) is M2( the carrier of L)
(L,(((a `) `) + (b `)),(((X `) `) + (b `))) is M2( the carrier of L)
the of L . ((((a `) `) + (b `)),(((X `) `) + (b `))) is M2( the carrier of L)
(L,(a `),b) is M2( the carrier of L)
the of L . ((a `),b) is M2( the carrier of L)
(L,(L,(a `),b),(((X `) `) + (b `))) is M2( the carrier of L)
the of L . ((L,(a `),b),(((X `) `) + (b `))) is M2( the carrier of L)
(L,(X `),b) is M2( the carrier of L)
the of L . ((X `),b) is M2( the carrier of L)
(L,(L,(a `),b),(L,(X `),b)) is M2( the carrier of L)
the of L . ((L,(a `),b),(L,(X `),b)) is M2( the carrier of L)
(L,(L,(L,a,a),b),(L,(X `),b)) is M2( the carrier of L)
the of L . ((L,(L,a,a),b),(L,(X `),b)) is M2( the carrier of L)
L is non empty ()
the carrier of L is non empty set
b is M2( the carrier of L)
(L,b,b) is M2( the carrier of L)
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the of L . (b,b) is M2( the carrier of L)
L is non empty () ()
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
X is M2( the carrier of L)
(L,a,X) is M2( the carrier of L)
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the of L . (a,X) is M2( the carrier of L)
(L,b,(L,a,X)) is M2( the carrier of L)
the of L . (b,(L,a,X)) is M2( the carrier of L)
(L,(L,b,(L,a,X))) is M2( the carrier of L)
(L,(L,b,(L,a,X)),(L,b,(L,a,X))) is M2( the carrier of L)
the of L . ((L,b,(L,a,X)),(L,b,(L,a,X))) is M2( the carrier of L)
(L,a) is M2( the carrier of L)
(L,a,a) is M2( the carrier of L)
the of L . (a,a) is M2( the carrier of L)
(L,(L,a),b) is M2( the carrier of L)
the of L . ((L,a),b) is M2( the carrier of L)
(L,X) is M2( the carrier of L)
(L,X,X) is M2( the carrier of L)
the of L . (X,X) is M2( the carrier of L)
(L,(L,X),b) is M2( the carrier of L)
the of L . ((L,X),b) is M2( the carrier of L)
(L,(L,(L,a),b),(L,(L,X),b)) is M2( the carrier of L)
the of L . ((L,(L,a),b),(L,(L,X),b)) is M2( the carrier of L)
L is non empty () ()
the carrier of L is non empty set
b is M2( the carrier of L)
(L,b) is M2( the carrier of L)
(L,b,b) is M2( the carrier of L)
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the of L . (b,b) is M2( the carrier of L)
(L,(L,b)) is M2( the carrier of L)
(L,(L,b),(L,b)) is M2( the carrier of L)
the of L . ((L,b),(L,b)) is M2( the carrier of L)
L is non empty () () () () ()
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
(L,b,a) is M2( the carrier of L)
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the of L . (b,a) is M2( the carrier of L)
(L,a,b) is M2( the carrier of L)
the of L . (a,b) is M2( the carrier of L)
(L,(L,b,a)) is M2( the carrier of L)
(L,(L,b,a),(L,b,a)) is M2( the carrier of L)
the of L . ((L,b,a),(L,b,a)) is M2( the carrier of L)
(L,(L,(L,b,a))) is M2( the carrier of L)
(L,(L,(L,b,a)),(L,(L,b,a))) is M2( the carrier of L)
the of L . ((L,(L,b,a)),(L,(L,b,a))) is M2( the carrier of L)
(L,a) is M2( the carrier of L)
(L,a,a) is M2( the carrier of L)
the of L . (a,a) is M2( the carrier of L)
(L,(L,a)) is M2( the carrier of L)
(L,(L,a),(L,a)) is M2( the carrier of L)
the of L . ((L,a),(L,a)) is M2( the carrier of L)
(L,b,(L,(L,a))) is M2( the carrier of L)
the of L . (b,(L,(L,a))) is M2( the carrier of L)
(L,(L,b,(L,(L,a)))) is M2( the carrier of L)
(L,(L,b,(L,(L,a))),(L,b,(L,(L,a)))) is M2( the carrier of L)
the of L . ((L,b,(L,(L,a))),(L,b,(L,(L,a)))) is M2( the carrier of L)
(L,(L,(L,b,(L,(L,a))))) is M2( the carrier of L)
(L,(L,(L,b,(L,(L,a)))),(L,(L,b,(L,(L,a))))) is M2( the carrier of L)
the of L . ((L,(L,b,(L,(L,a)))),(L,(L,b,(L,(L,a))))) is M2( the carrier of L)
(L,(L,(L,a)),b) is M2( the carrier of L)
the of L . ((L,(L,a)),b) is M2( the carrier of L)
(L,(L,(L,(L,a)),b)) is M2( the carrier of L)
(L,(L,(L,(L,a)),b),(L,(L,(L,a)),b)) is M2( the carrier of L)
the of L . ((L,(L,(L,a)),b),(L,(L,(L,a)),b)) is M2( the carrier of L)
(L,(L,(L,(L,(L,a)),b))) is M2( the carrier of L)
(L,(L,(L,(L,(L,a)),b)),(L,(L,(L,(L,a)),b))) is M2( the carrier of L)
the of L . ((L,(L,(L,(L,a)),b)),(L,(L,(L,(L,a)),b))) is M2( the carrier of L)
(L,(L,a,b)) is M2( the carrier of L)
(L,(L,a,b),(L,a,b)) is M2( the carrier of L)
the of L . ((L,a,b),(L,a,b)) is M2( the carrier of L)
(L,(L,(L,a,b))) is M2( the carrier of L)
(L,(L,(L,a,b)),(L,(L,a,b))) is M2( the carrier of L)
the of L . ((L,(L,a,b)),(L,(L,a,b))) is M2( the carrier of L)
L is non empty () () () () ()
the carrier of L is non empty set
b is M2( the carrier of L)
(L,b,b) is M2( the carrier of L)
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the of L . (b,b) is M2( the carrier of L)
(L,b,(L,b,b)) is M2( the carrier of L)
the of L . (b,(L,b,b)) is M2( the carrier of L)
a is M2( the carrier of L)
(L,a,a) is M2( the carrier of L)
the of L . (a,a) is M2( the carrier of L)
(L,a,(L,a,a)) is M2( the carrier of L)
the of L . (a,(L,a,a)) is M2( the carrier of L)
(L,b) is M2( the carrier of L)
(L,b,(L,b)) is M2( the carrier of L)
the of L . (b,(L,b)) is M2( the carrier of L)
(L,(L,b,(L,b)),(L,b,(L,b))) is M2( the carrier of L)
the of L . ((L,b,(L,b)),(L,b,(L,b))) is M2( the carrier of L)
(L,(L,(L,b,(L,b)),(L,b,(L,b)))) is M2( the carrier of L)
(L,(L,(L,b,(L,b)),(L,b,(L,b))),(L,(L,b,(L,b)),(L,b,(L,b)))) is M2( the carrier of L)
the of L . ((L,(L,b,(L,b)),(L,b,(L,b))),(L,(L,b,(L,b)),(L,b,(L,b)))) is M2( the carrier of L)
(L,a) is M2( the carrier of L)
(L,a,(L,a)) is M2( the carrier of L)
the of L . (a,(L,a)) is M2( the carrier of L)
(L,(L,b,(L,b)),(L,a,(L,a))) is M2( the carrier of L)
the of L . ((L,b,(L,b)),(L,a,(L,a))) is M2( the carrier of L)
(L,(L,(L,b,(L,b)),(L,a,(L,a)))) is M2( the carrier of L)
(L,(L,(L,b,(L,b)),(L,a,(L,a))),(L,(L,b,(L,b)),(L,a,(L,a)))) is M2( the carrier of L)
the of L . ((L,(L,b,(L,b)),(L,a,(L,a))),(L,(L,b,(L,b)),(L,a,(L,a)))) is M2( the carrier of L)
(L,(L,a,(L,a)),(L,b,(L,b,b))) is M2( the carrier of L)
the of L . ((L,a,(L,a)),(L,b,(L,b,b))) is M2( the carrier of L)
(L,(L,(L,a,(L,a)),(L,b,(L,b,b)))) is M2( the carrier of L)
(L,(L,(L,a,(L,a)),(L,b,(L,b,b))),(L,(L,a,(L,a)),(L,b,(L,b,b)))) is M2( the carrier of L)
the of L . ((L,(L,a,(L,a)),(L,b,(L,b,b))),(L,(L,a,(L,a)),(L,b,(L,b,b)))) is M2( the carrier of L)
(L,(L,a,(L,a))) is M2( the carrier of L)
(L,(L,a,(L,a)),(L,a,(L,a))) is M2( the carrier of L)
the of L . ((L,a,(L,a)),(L,a,(L,a))) is M2( the carrier of L)
(L,(L,(L,a,(L,a)))) is M2( the carrier of L)
(L,(L,(L,a,(L,a))),(L,(L,a,(L,a)))) is M2( the carrier of L)
the of L . ((L,(L,a,(L,a))),(L,(L,a,(L,a)))) is M2( the carrier of L)
L is non empty () () () () ()
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
b "\/" a is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . (b,a) is M2( the carrier of L)
a "\/" b is M2( the carrier of L)
the L_join of L . (a,b) is M2( the carrier of L)
(L,b) is M2( the carrier of L)
(L,b,b) is M2( the carrier of L)
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the of L . (b,b) is M2( the carrier of L)
(L,a,a) is M2( the carrier of L)
the of L . (a,a) is M2( the carrier of L)
(L,(L,b),(L,a,a)) is M2( the carrier of L)
the of L . ((L,b),(L,a,a)) is M2( the carrier of L)
(L,(L,a,a),(L,b,b)) is M2( the carrier of L)
the of L . ((L,a,a),(L,b,b)) is M2( the carrier of L)
L is non empty () () () () ()
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
b "/\" a is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . (b,a) is M2( the carrier of L)
a "/\" b is M2( the carrier of L)
the L_meet of L . (a,b) is M2( the carrier of L)
(L,b,a) is M2( the carrier of L)
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the of L . (b,a) is M2( the carrier of L)
(L,(L,b,a),(L,b,a)) is M2( the carrier of L)
the of L . ((L,b,a),(L,b,a)) is M2( the carrier of L)
(L,a,b) is M2( the carrier of L)
the of L . (a,b) is M2( the carrier of L)
(L,(L,a,b),(L,b,a)) is M2( the carrier of L)
the of L . ((L,a,b),(L,b,a)) is M2( the carrier of L)
(L,(L,a,b),(L,a,b)) is M2( the carrier of L)
the of L . ((L,a,b),(L,a,b)) is M2( the carrier of L)
L is non empty () () () () ()
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
X is M2( the carrier of L)
a "\/" X is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_join of L . (a,X) is M2( the carrier of L)
b "/\" (a "\/" X) is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_meet of L . (b,(a "\/" X)) is M2( the carrier of L)
b "/\" a is M2( the carrier of L)
the L_meet of L . (b,a) is M2( the carrier of L)
b "/\" X is M2( the carrier of L)
the L_meet of L . (b,X) is M2( the carrier of L)
(b "/\" a) "\/" (b "/\" X) is M2( the carrier of L)
the L_join of L . ((b "/\" a),(b "/\" X)) is M2( the carrier of L)
(L,a) is M2( the carrier of L)
(L,a,a) is M2( the carrier of L)
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the of L . (a,a) is M2( the carrier of L)
(L,X) is M2( the carrier of L)
(L,X,X) is M2( the carrier of L)
the of L . (X,X) is M2( the carrier of L)
(L,(L,a,a),(L,X,X)) is M2( the carrier of L)
the of L . ((L,a,a),(L,X,X)) is M2( the carrier of L)
b "/\" (L,(L,a,a),(L,X,X)) is M2( the carrier of L)
the L_meet of L . (b,(L,(L,a,a),(L,X,X))) is M2( the carrier of L)
(L,(L,a),(L,X)) is M2( the carrier of L)
the of L . ((L,a),(L,X)) is M2( the carrier of L)
(L,b,(L,(L,a),(L,X))) is M2( the carrier of L)
the of L . (b,(L,(L,a),(L,X))) is M2( the carrier of L)
(L,(L,b,(L,(L,a),(L,X)))) is M2( the carrier of L)
(L,(L,b,(L,(L,a),(L,X))),(L,b,(L,(L,a),(L,X)))) is M2( the carrier of L)
the of L . ((L,b,(L,(L,a),(L,X))),(L,b,(L,(L,a),(L,X)))) is M2( the carrier of L)
(L,(L,a)) is M2( the carrier of L)
(L,(L,a),(L,a)) is M2( the carrier of L)
the of L . ((L,a),(L,a)) is M2( the carrier of L)
(L,(L,(L,a)),b) is M2( the carrier of L)
the of L . ((L,(L,a)),b) is M2( the carrier of L)
(L,(L,X)) is M2( the carrier of L)
(L,(L,X),(L,X)) is M2( the carrier of L)
the of L . ((L,X),(L,X)) is M2( the carrier of L)
(L,(L,(L,X)),b) is M2( the carrier of L)
the of L . ((L,(L,X)),b) is M2( the carrier of L)
(L,(L,(L,(L,a)),b),(L,(L,(L,X)),b)) is M2( the carrier of L)
the of L . ((L,(L,(L,a)),b),(L,(L,(L,X)),b)) is M2( the carrier of L)
(L,a,b) is M2( the carrier of L)
the of L . (a,b) is M2( the carrier of L)
(L,(L,a,b),(L,(L,(L,X)),b)) is M2( the carrier of L)
the of L . ((L,a,b),(L,(L,(L,X)),b)) is M2( the carrier of L)
(L,X,b) is M2( the carrier of L)
the of L . (X,b) is M2( the carrier of L)
(L,(L,a,b),(L,X,b)) is M2( the carrier of L)
the of L . ((L,a,b),(L,X,b)) is M2( the carrier of L)
(L,b,a) is M2( the carrier of L)
the of L . (b,a) is M2( the carrier of L)
(L,(L,b,a),(L,X,b)) is M2( the carrier of L)
the of L . ((L,b,a),(L,X,b)) is M2( the carrier of L)
(L,b,X) is M2( the carrier of L)
the of L . (b,X) is M2( the carrier of L)
(L,(L,b,a),(L,b,X)) is M2( the carrier of L)
the of L . ((L,b,a),(L,b,X)) is M2( the carrier of L)
(L,(L,b,a)) is M2( the carrier of L)
(L,(L,b,a),(L,b,a)) is M2( the carrier of L)
the of L . ((L,b,a),(L,b,a)) is M2( the carrier of L)
(L,(L,(L,b,a))) is M2( the carrier of L)
(L,(L,(L,b,a)),(L,(L,b,a))) is M2( the carrier of L)
the of L . ((L,(L,b,a)),(L,(L,b,a))) is M2( the carrier of L)
(L,(L,(L,(L,b,a))),(L,b,X)) is M2( the carrier of L)
the of L . ((L,(L,(L,b,a))),(L,b,X)) is M2( the carrier of L)
(L,(L,(L,b,a),(L,b,a))) is M2( the carrier of L)
(L,(L,(L,b,a),(L,b,a)),(L,(L,b,a),(L,b,a))) is M2( the carrier of L)
the of L . ((L,(L,b,a),(L,b,a)),(L,(L,b,a),(L,b,a))) is M2( the carrier of L)
(L,(L,b,X)) is M2( the carrier of L)
(L,(L,b,X),(L,b,X)) is M2( the carrier of L)
the of L . ((L,b,X),(L,b,X)) is M2( the carrier of L)
(L,(L,(L,b,X))) is M2( the carrier of L)
(L,(L,(L,b,X)),(L,(L,b,X))) is M2( the carrier of L)
the of L . ((L,(L,b,X)),(L,(L,b,X))) is M2( the carrier of L)
(L,(L,(L,(L,b,a),(L,b,a))),(L,(L,(L,b,X)))) is M2( the carrier of L)
the of L . ((L,(L,(L,b,a),(L,b,a))),(L,(L,(L,b,X)))) is M2( the carrier of L)
(L,(b "/\" a),(L,(L,b,a),(L,b,a))) is M2( the carrier of L)
the of L . ((b "/\" a),(L,(L,b,a),(L,b,a))) is M2( the carrier of L)
(L,(L,(L,b,X),(L,b,X)),(L,(L,b,X),(L,b,X))) is M2( the carrier of L)
the of L . ((L,(L,b,X),(L,b,X)),(L,(L,b,X),(L,b,X))) is M2( the carrier of L)
(L,(L,(b "/\" a),(L,(L,b,a),(L,b,a))),(L,(L,(L,b,X),(L,b,X)),(L,(L,b,X),(L,b,X)))) is M2( the carrier of L)
the of L . ((L,(b "/\" a),(L,(L,b,a),(L,b,a))),(L,(L,(L,b,X),(L,b,X)),(L,(L,b,X),(L,b,X)))) is M2( the carrier of L)
(L,(b "/\" a),(b "/\" a)) is M2( the carrier of L)
the of L . ((b "/\" a),(b "/\" a)) is M2( the carrier of L)
(L,(L,(b "/\" a),(b "/\" a)),(L,(L,(L,b,X),(L,b,X)),(L,(L,b,X),(L,b,X)))) is M2( the carrier of L)
the of L . ((L,(b "/\" a),(b "/\" a)),(L,(L,(L,b,X),(L,b,X)),(L,(L,b,X),(L,b,X)))) is M2( the carrier of L)
(L,(b "/\" X),(L,(L,b,X),(L,b,X))) is M2( the carrier of L)
the of L . ((b "/\" X),(L,(L,b,X),(L,b,X))) is M2( the carrier of L)
(L,(L,(b "/\" a),(b "/\" a)),(L,(b "/\" X),(L,(L,b,X),(L,b,X)))) is M2( the carrier of L)
the of L . ((L,(b "/\" a),(b "/\" a)),(L,(b "/\" X),(L,(L,b,X),(L,b,X)))) is M2( the carrier of L)
(L,(b "/\" X),(b "/\" X)) is M2( the carrier of L)
the of L . ((b "/\" X),(b "/\" X)) is M2( the carrier of L)
(L,(L,(b "/\" a),(b "/\" a)),(L,(b "/\" X),(b "/\" X))) is M2( the carrier of L)
the of L . ((L,(b "/\" a),(b "/\" a)),(L,(b "/\" X),(b "/\" X))) is M2( the carrier of L)
L is non empty () () () () ()
the carrier of L is non empty set
b is M2( the carrier of L)
a is M2( the carrier of L)
X is M2( the carrier of L)
a "/\" X is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the L_meet of L . (a,X) is M2( the carrier of L)
b "\/" (a "/\" X) is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_join of L . (b,(a "/\" X)) is M2( the carrier of L)
b "\/" a is M2( the carrier of L)
the L_join of L . (b,a) is M2( the carrier of L)
b "\/" X is M2( the carrier of L)
the L_join of L . (b,X) is M2( the carrier of L)
(b "\/" a) "/\" (b "\/" X) is M2( the carrier of L)
the L_meet of L . ((b "\/" a),(b "\/" X)) is M2( the carrier of L)
(L,b,b) is M2( the carrier of L)
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the of L . (b,b) is M2( the carrier of L)
(L,a,X) is M2( the carrier of L)
the of L . (a,X) is M2( the carrier of L)
(L,(L,a,X),(L,a,X)) is M2( the carrier of L)
the of L . ((L,a,X),(L,a,X)) is M2( the carrier of L)
b "\/" (L,(L,a,X),(L,a,X)) is M2( the carrier of L)
the L_join of L . (b,(L,(L,a,X),(L,a,X))) is M2( the carrier of L)
(L,(L,a,X)) is M2( the carrier of L)
(L,(L,(L,a,X))) is M2( the carrier of L)
(L,(L,(L,a,X)),(L,(L,a,X))) is M2( the carrier of L)
the of L . ((L,(L,a,X)),(L,(L,a,X))) is M2( the carrier of L)
(L,(L,b,b),(L,(L,(L,a,X)))) is M2( the carrier of L)
the of L . ((L,b,b),(L,(L,(L,a,X)))) is M2( the carrier of L)
(L,(L,b,b),(L,a,X)) is M2( the carrier of L)
the of L . ((L,b,b),(L,a,X)) is M2( the carrier of L)
(L,(L,(L,b,b),(L,a,X))) is M2( the carrier of L)
(L,(L,(L,b,b),(L,a,X)),(L,(L,b,b),(L,a,X))) is M2( the carrier of L)
the of L . ((L,(L,b,b),(L,a,X)),(L,(L,b,b),(L,a,X))) is M2( the carrier of L)
(L,(L,(L,(L,b,b),(L,a,X)))) is M2( the carrier of L)
(L,(L,(L,(L,b,b),(L,a,X))),(L,(L,(L,b,b),(L,a,X)))) is M2( the carrier of L)
the of L . ((L,(L,(L,b,b),(L,a,X))),(L,(L,(L,b,b),(L,a,X)))) is M2( the carrier of L)
(L,a) is M2( the carrier of L)
(L,a,a) is M2( the carrier of L)
the of L . (a,a) is M2( the carrier of L)
(L,(L,a),(L,b,b)) is M2( the carrier of L)
the of L . ((L,a),(L,b,b)) is M2( the carrier of L)
(L,X) is M2( the carrier of L)
(L,X,X) is M2( the carrier of L)
the of L . (X,X) is M2( the carrier of L)
(L,(L,X),(L,b,b)) is M2( the carrier of L)
the of L . ((L,X),(L,b,b)) is M2( the carrier of L)
(L,(L,(L,a),(L,b,b)),(L,(L,X),(L,b,b))) is M2( the carrier of L)
the of L . ((L,(L,a),(L,b,b)),(L,(L,X),(L,b,b))) is M2( the carrier of L)
(L,(L,(L,(L,a),(L,b,b)),(L,(L,X),(L,b,b)))) is M2( the carrier of L)
(L,(L,(L,(L,a),(L,b,b)),(L,(L,X),(L,b,b))),(L,(L,(L,a),(L,b,b)),(L,(L,X),(L,b,b)))) is M2( the carrier of L)
the of L . ((L,(L,(L,a),(L,b,b)),(L,(L,X),(L,b,b))),(L,(L,(L,a),(L,b,b)),(L,(L,X),(L,b,b)))) is M2( the carrier of L)
(L,(L,b,b),(L,a)) is M2( the carrier of L)
the of L . ((L,b,b),(L,a)) is M2( the carrier of L)
(L,(L,(L,b,b),(L,a)),(L,(L,X),(L,b,b))) is M2( the carrier of L)
the of L . ((L,(L,b,b),(L,a)),(L,(L,X),(L,b,b))) is M2( the carrier of L)
(L,(L,(L,(L,b,b),(L,a)),(L,(L,X),(L,b,b)))) is M2( the carrier of L)
(L,(L,(L,(L,b,b),(L,a)),(L,(L,X),(L,b,b))),(L,(L,(L,b,b),(L,a)),(L,(L,X),(L,b,b)))) is M2( the carrier of L)
the of L . ((L,(L,(L,b,b),(L,a)),(L,(L,X),(L,b,b))),(L,(L,(L,b,b),(L,a)),(L,(L,X),(L,b,b)))) is M2( the carrier of L)
(L,(L,b,b),(L,a,a)) is M2( the carrier of L)
the of L . ((L,b,b),(L,a,a)) is M2( the carrier of L)
(L,(L,b,b),(L,X)) is M2( the carrier of L)
the of L . ((L,b,b),(L,X)) is M2( the carrier of L)
(L,(L,(L,b,b),(L,a,a)),(L,(L,b,b),(L,X))) is M2( the carrier of L)
the of L . ((L,(L,b,b),(L,a,a)),(L,(L,b,b),(L,X))) is M2( the carrier of L)
(L,(L,(L,(L,b,b),(L,a,a)),(L,(L,b,b),(L,X)))) is M2( the carrier of L)
(L,(L,(L,(L,b,b),(L,a,a)),(L,(L,b,b),(L,X))),(L,(L,(L,b,b),(L,a,a)),(L,(L,b,b),(L,X)))) is M2( the carrier of L)
the of L . ((L,(L,(L,b,b),(L,a,a)),(L,(L,b,b),(L,X))),(L,(L,(L,b,b),(L,a,a)),(L,(L,b,b),(L,X)))) is M2( the carrier of L)
(L,(L,b,b),(L,X,X)) is M2( the carrier of L)
the of L . ((L,b,b),(L,X,X)) is M2( the carrier of L)
(L,(b "\/" a),(L,(L,b,b),(L,X,X))) is M2( the carrier of L)
the of L . ((b "\/" a),(L,(L,b,b),(L,X,X))) is M2( the carrier of L)
(L,(L,(L,b,b),(L,a,a)),(L,(L,b,b),(L,X,X))) is M2( the carrier of L)
the of L . ((L,(L,b,b),(L,a,a)),(L,(L,b,b),(L,X,X))) is M2( the carrier of L)
(L,(L,(b "\/" a),(L,(L,b,b),(L,X,X))),(L,(L,(L,b,b),(L,a,a)),(L,(L,b,b),(L,X,X)))) is M2( the carrier of L)
the of L . ((L,(b "\/" a),(L,(L,b,b),(L,X,X))),(L,(L,(L,b,b),(L,a,a)),(L,(L,b,b),(L,X,X)))) is M2( the carrier of L)
(L,(b "\/" a),(b "\/" X)) is M2( the carrier of L)
the of L . ((b "\/" a),(b "\/" X)) is M2( the carrier of L)
(L,(L,(b "\/" a),(b "\/" X)),(L,(L,(L,b,b),(L,a,a)),(L,(L,b,b),(L,X,X)))) is M2( the carrier of L)
the of L . ((L,(b "\/" a),(b "\/" X)),(L,(L,(L,b,b),(L,a,a)),(L,(L,b,b),(L,X,X)))) is M2( the carrier of L)
(L,(L,(b "\/" a),(b "\/" X)),(L,(b "\/" a),(L,(L,b,b),(L,X,X)))) is M2( the carrier of L)
the of L . ((L,(b "\/" a),(b "\/" X)),(L,(b "\/" a),(L,(L,b,b),(L,X,X)))) is M2( the carrier of L)
(L,(L,(b "\/" a),(b "\/" X)),(L,(b "\/" a),(b "\/" X))) is M2( the carrier of L)
the of L . ((L,(b "\/" a),(b "\/" X)),(L,(b "\/" a),(b "\/" X))) is M2( the carrier of L)
L is non empty () () () () ()
the carrier of L is non empty set
the M2( the carrier of L) is M2( the carrier of L)
(L, the M2( the carrier of L), the M2( the carrier of L)) is M2( the carrier of L)
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the of L . ( the M2( the carrier of L), the M2( the carrier of L)) is M2( the carrier of L)
(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L, the M2( the carrier of L), the M2( the carrier of L))) is M2( the carrier of L)
the of L . ((L, the M2( the carrier of L), the M2( the carrier of L)),(L, the M2( the carrier of L), the M2( the carrier of L))) is M2( the carrier of L)
(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L, the M2( the carrier of L), the M2( the carrier of L)))) is M2( the carrier of L)
the of L . ((L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L, the M2( the carrier of L), the M2( the carrier of L)))) is M2( the carrier of L)
a is M2( the carrier of L)
X is M2( the carrier of L)
a "/\" X is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_meet of L . (a,X) is M2( the carrier of L)
X "/\" a is M2( the carrier of L)
the L_meet of L . (X,a) is M2( the carrier of L)
(L, the M2( the carrier of L)) is M2( the carrier of L)
(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L))) is M2( the carrier of L)
the of L . ((L, the M2( the carrier of L)),(L, the M2( the carrier of L))) is M2( the carrier of L)
(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))) is M2( the carrier of L)
the of L . ((L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))) is M2( the carrier of L)
(L,(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))),X) is M2( the carrier of L)
the of L . ((L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))),X) is M2( the carrier of L)
(L,(L,(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))),X)) is M2( the carrier of L)
(L,(L,(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))),X),(L,(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))),X)) is M2( the carrier of L)
the of L . ((L,(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))),X),(L,(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))),X)) is M2( the carrier of L)
(L,(L, the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))) is M2( the carrier of L)
the of L . ((L, the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))) is M2( the carrier of L)
(L,X,(L,(L, the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L))))) is M2( the carrier of L)
the of L . (X,(L,(L, the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L))))) is M2( the carrier of L)
(L,(L,X,(L,(L, the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))))) is M2( the carrier of L)
(L,(L,X,(L,(L, the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L))))),(L,X,(L,(L, the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))))) is M2( the carrier of L)
the of L . ((L,X,(L,(L, the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L))))),(L,X,(L,(L, the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))))) is M2( the carrier of L)
(L,X,X) is M2( the carrier of L)
the of L . (X,X) is M2( the carrier of L)
(L,(L,X,X)) is M2( the carrier of L)
(L,(L,X,X),(L,X,X)) is M2( the carrier of L)
the of L . ((L,X,X),(L,X,X)) is M2( the carrier of L)
(L, the M2( the carrier of L)) is M2( the carrier of L)
(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L))) is M2( the carrier of L)
the of L . ((L, the M2( the carrier of L)),(L, the M2( the carrier of L))) is M2( the carrier of L)
(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))) is M2( the carrier of L)
the of L . ((L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))) is M2( the carrier of L)
(L,X,(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L))))) is M2( the carrier of L)
the of L . (X,(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L))))) is M2( the carrier of L)
(L,(L,X,(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))))) is M2( the carrier of L)
(L,(L,X,(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L))))),(L,X,(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))))) is M2( the carrier of L)
the of L . ((L,X,(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L))))),(L,X,(L,(L, the M2( the carrier of L), the M2( the carrier of L)),(L,(L, the M2( the carrier of L)),(L, the M2( the carrier of L)))))) is M2( the carrier of L)
(L,X,X) is M2( the carrier of L)
the of L . (X,X) is M2( the carrier of L)
(L,(L,X,X)) is M2( the carrier of L)
(L,(L,X,X),(L,X,X)) is M2( the carrier of L)
the of L . ((L,X,X),(L,X,X)) is M2( the carrier of L)
b is M2( the carrier of L)
the M2( the carrier of L) is M2( the carrier of L)
(L, the M2( the carrier of L), the M2( the carrier of L)) is M2( the carrier of L)
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the of L . ( the M2( the carrier of L), the M2( the carrier of L)) is M2( the carrier of L)
(L, the M2( the carrier of L),(L, the M2( the carrier of L), the M2( the carrier of L))) is M2( the carrier of L)
the of L . ( the M2( the carrier of L),(L, the M2( the carrier of L), the M2( the carrier of L))) is M2( the carrier of L)
(L,(L, the M2( the carrier of L),(L, the M2( the carrier of L), the M2( the carrier of L))),(L, the M2( the carrier of L),(L, the M2( the carrier of L), the M2( the carrier of L)))) is M2( the carrier of L)
the of L . ((L, the M2( the carrier of L),(L, the M2( the carrier of L), the M2( the carrier of L))),(L, the M2( the carrier of L),(L, the M2( the carrier of L), the M2( the carrier of L)))) is M2( the carrier of L)
a is M2( the carrier of L)
X is M2( the carrier of L)
a "\/" X is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_join of L . (a,X) is M2( the carrier of L)
X "\/" a is M2( the carrier of L)
the L_join of L . (X,a) is M2( the carrier of L)
(L,(L, the M2( the carrier of L),(L, the M2( the carrier of L), the M2( the carrier of L)))) is M2( the carrier of L)
(L,(L,(L, the M2( the carrier of L),(L, the M2( the carrier of L), the M2( the carrier of L))))) is M2( the carrier of L)
(L,(L,(L, the M2( the carrier of L),(L, the M2( the carrier of L), the M2( the carrier of L)))),(L,(L, the M2( the carrier of L),(L, the M2( the carrier of L), the M2( the carrier of L))))) is M2( the carrier of L)
the of L . ((L,(L, the M2( the carrier of L),(L, the M2( the carrier of L), the M2( the carrier of L)))),(L,(L, the M2( the carrier of L),(L, the M2( the carrier of L), the M2( the carrier of L))))) is M2( the carrier of L)
(L,X,X) is M2( the carrier of L)
the of L . (X,X) is M2( the carrier of L)
(L,(L,(L,(L, the M2( the carrier of L),(L, the M2( the carrier of L), the M2( the carrier of L))))),(L,X,X)) is M2( the carrier of L)
the of L . ((L,(L,(L, the M2( the carrier of L),(L, the M2( the carrier of L), the M2( the carrier of L))))),(L,X,X)) is M2( the carrier of L)
(L,X,(L,X,X)) is M2( the carrier of L)
the of L . (X,(L,X,X)) is M2( the carrier of L)
(L,(L,X,(L,X,X))) is M2( the carrier of L)
(L,(L,X,(L,X,X)),(L,X,(L,X,X))) is M2( the carrier of L)
the of L . ((L,X,(L,X,X)),(L,X,(L,X,X))) is M2( the carrier of L)
(L,(L,(L,X,(L,X,X)))) is M2( the carrier of L)
(L,(L,(L,X,(L,X,X))),(L,(L,X,(L,X,X)))) is M2( the carrier of L)
the of L . ((L,(L,X,(L,X,X))),(L,(L,X,(L,X,X)))) is M2( the carrier of L)
(L,(L,(L,(L,X,(L,X,X)))),(L,X,X)) is M2( the carrier of L)
the of L . ((L,(L,(L,X,(L,X,X)))),(L,X,X)) is M2( the carrier of L)
(L,(L,X,(L,X,X)),(L,X,X)) is M2( the carrier of L)
the of L . ((L,X,(L,X,X)),(L,X,X)) is M2( the carrier of L)
(L,(L,X,X),(L,X,(L,X,X))) is M2( the carrier of L)
the of L . ((L,X,X),(L,X,(L,X,X))) is M2( the carrier of L)
(L,(L,X,X),(L,X,X)) is M2( the carrier of L)
the of L . ((L,X,X),(L,X,X)) is M2( the carrier of L)
(L,(L,X,X),(L,(L,(L, the M2( the carrier of L),(L, the M2( the carrier of L), the M2( the carrier of L)))))) is M2( the carrier of L)
the of L . ((L,X,X),(L,(L,(L, the M2( the carrier of L),(L, the M2( the carrier of L), the M2( the carrier of L)))))) is M2( the carrier of L)
(L,(L,X,X),(L,(L,(L,X,(L,X,X))))) is M2( the carrier of L)
the of L . ((L,X,X),(L,(L,(L,X,(L,X,X))))) is M2( the carrier of L)
b is M2( the carrier of L)
b is M2( the carrier of L)
(L,b,b) is M2( the carrier of L)
the of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
K20( the carrier of L, the carrier of L) is set
K20(K20( the carrier of L, the carrier of L), the carrier of L) is set
K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set
the of L . (b,b) is M2( the carrier of L)
(L) is M2( the carrier of L)
(L,(L,b,b),(L,b,b)) is M2( the carrier of L)
the of L . ((L,b,b),(L,b,b)) is M2( the carrier of L)
(L,(L,b,b),(L,(L,b,b),(L,b,b))) is M2( the carrier of L)
the of L . ((L,b,b),(L,(L,b,b),(L,b,b))) is M2( the carrier of L)
a is M2( the carrier of L)
(L,(L,b,b),(L,(L,b,b),(L,b,b))) "/\" a is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_meet of L . ((L,(L,b,b),(L,(L,b,b),(L,b,b))),a) is M2( the carrier of L)
a "/\" (L,(L,b,b),(L,(L,b,b),(L,b,b))) is M2( the carrier of L)
the L_meet of L . (a,(L,(L,b,b),(L,(L,b,b),(L,b,b)))) is M2( the carrier of L)
(L,b) is M2( the carrier of L)
(L,(L,b),(L,b)) is M2( the carrier of L)
the of L . ((L,b),(L,b)) is M2( the carrier of L)
(L,(L,b,b),(L,(L,b),(L,b))) is M2( the carrier of L)
the of L . ((L,b,b),(L,(L,b),(L,b))) is M2( the carrier of L)
(L,(L,(L,b,b),(L,(L,b),(L,b))),a) is M2( the carrier of L)
the of L . ((L,(L,b,b),(L,(L,b),(L,b))),a) is M2( the carrier of L)
(L,(L,(L,(L,b,b),(L,(L,b),(L,b))),a)) is M2( the carrier of L)
(L,(L,(L,(L,b,b),(L,(L,b),(L,b))),a),(L,(L,(L,b,b),(L,(L,b),(L,b))),a)) is M2( the carrier of L)
the of L . ((L,(L,(L,b,b),(L,(L,b),(L,b))),a),(L,(L,(L,b,b),(L,(L,b),(L,b))),a)) is M2( the carrier of L)
(L,(L,b),(L,(L,b),(L,b))) is M2( the carrier of L)
the of L . ((L,b),(L,(L,b),(L,b))) is M2( the carrier of L)
(L,a,(L,(L,b),(L,(L,b),(L,b)))) is M2( the carrier of L)
the of L . (a,(L,(L,b),(L,(L,b),(L,b)))) is M2( the carrier of L)
(L,(L,a,(L,(L,b),(L,(L,b),(L,b))))) is M2( the carrier of L)
(L,(L,a,(L,(L,b),(L,(L,b),(L,b)))),(L,a,(L,(L,b),(L,(L,b),(L,b))))) is M2( the carrier of L)
the of L . ((L,a,(L,(L,b),(L,(L,b),(L,b)))),(L,a,(L,(L,b),(L,(L,b),(L,b))))) is M2( the carrier of L)
(L,a,a) is M2( the carrier of L)
the of L . (a,a) is M2( the carrier of L)
(L,(L,a,a)) is M2( the carrier of L)
(L,(L,a,a),(L,a,a)) is M2( the carrier of L)
the of L . ((L,a,a),(L,a,a)) is M2( the carrier of L)
(L,a,(L,(L,b,b),(L,(L,b),(L,b)))) is M2( the carrier of L)
the of L . (a,(L,(L,b,b),(L,(L,b),(L,b)))) is M2( the carrier of L)
(L,(L,a,(L,(L,b,b),(L,(L,b),(L,b))))) is M2( the carrier of L)
(L,(L,a,(L,(L,b,b),(L,(L,b),(L,b)))),(L,a,(L,(L,b,b),(L,(L,b),(L,b))))) is M2( the carrier of L)
the of L . ((L,a,(L,(L,b,b),(L,(L,b),(L,b)))),(L,a,(L,(L,b,b),(L,(L,b),(L,b))))) is M2( the carrier of L)
b "\/" (L,b,b) is M2( the carrier of L)
the L_join of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_join of L . (b,(L,b,b)) is M2( the carrier of L)
(L) is M2( the carrier of L)
(L,b,(L,b,b)) is M2( the carrier of L)
the of L . (b,(L,b,b)) is M2( the carrier of L)
(L,(L,b,(L,b,b)),(L,b,(L,b,b))) is M2( the carrier of L)
the of L . ((L,b,(L,b,b)),(L,b,(L,b,b))) is M2( the carrier of L)
a is M2( the carrier of L)
(L,(L,b,(L,b,b)),(L,b,(L,b,b))) "\/" a is M2( the carrier of L)
the L_join of L . ((L,(L,b,(L,b,b)),(L,b,(L,b,b))),a) is M2( the carrier of L)
a "\/" (L,(L,b,(L,b,b)),(L,b,(L,b,b))) is M2( the carrier of L)
the L_join of L . (a,(L,(L,b,(L,b,b)),(L,b,(L,b,b)))) is M2( the carrier of L)
(L,(L,b,(L,b,b))) is M2( the carrier of L)
(L,(L,(L,b,(L,b,b)))) is M2( the carrier of L)
(L,(L,(L,b,(L,b,b))),(L,(L,b,(L,b,b)))) is M2( the carrier of L)
the of L . ((L,(L,b,(L,b,b))),(L,(L,b,(L,b,b)))) is M2( the carrier of L)
(L,a,a) is M2( the carrier of L)
the of L . (a,a) is M2( the carrier of L)
(L,(L,(L,(L,b,(L,b,b)))),(L,a,a)) is M2( the carrier of L)
the of L . ((L,(L,(L,b,(L,b,b)))),(L,a,a)) is M2( the carrier of L)
(L,a,(L,a,a)) is M2( the carrier of L)
the of L . (a,(L,a,a)) is M2( the carrier of L)
(L,(L,a,(L,a,a))) is M2( the carrier of L)
(L,(L,a,(L,a,a)),(L,a,(L,a,a))) is M2( the carrier of L)
the of L . ((L,a,(L,a,a)),(L,a,(L,a,a))) is M2( the carrier of L)
(L,(L,(L,a,(L,a,a)))) is M2( the carrier of L)
(L,(L,(L,a,(L,a,a))),(L,(L,a,(L,a,a)))) is M2( the carrier of L)
the of L . ((L,(L,a,(L,a,a))),(L,(L,a,(L,a,a)))) is M2( the carrier of L)
(L,(L,(L,(L,a,(L,a,a)))),(L,a,a)) is M2( the carrier of L)
the of L . ((L,(L,(L,a,(L,a,a)))),(L,a,a)) is M2( the carrier of L)
(L,(L,a,(L,a,a)),(L,a,a)) is M2( the carrier of L)
the of L . ((L,a,(L,a,a)),(L,a,a)) is M2( the carrier of L)
(L,(L,a,a),(L,a,(L,a,a))) is M2( the carrier of L)
the of L . ((L,a,a),(L,a,(L,a,a))) is M2( the carrier of L)
(L,(L,a,a),(L,a,a)) is M2( the carrier of L)
the of L . ((L,a,a),(L,a,a)) is M2( the carrier of L)
(L,(L,a,a),(L,(L,(L,b,(L,b,b))))) is M2( the carrier of L)
the of L . ((L,a,a),(L,(L,(L,b,(L,b,b))))) is M2( the carrier of L)
(L,(L,a,a),(L,(L,(L,a,(L,a,a))))) is M2( the carrier of L)
the of L . ((L,a,a),(L,(L,(L,a,(L,a,a))))) is M2( the carrier of L)
b "/\" (L,b,b) is M2( the carrier of L)
the L_meet of L is V6() V18(K20( the carrier of L, the carrier of L), the carrier of L) M2(K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)))
the L_meet of L . (b,(L,b,b)) is M2( the carrier of L)
(L,b,b) "\/" b is M2( the carrier of L)
the L_join of L . ((L,b,b),b) is M2( the carrier of L)
(L,(L,(L,b,b),(L,b,b)),(L,b,b)) is M2( the carrier of L)
the of L . ((L,(L,b,b),(L,b,b)),(L,b,b)) is M2( the carrier of L)
(L,b,b) "/\" b is M2( the carrier of L)
the L_meet of L . ((L,b,b),b) is M2( the carrier of L)
(L,(L,b,b),b) is M2( the carrier of L)
the of L . ((L,b,b),b) is M2( the carrier of L)
(L,(L,(L,b,b),b),(L,(L,b,b),b)) is M2( the carrier of L)
the of L . ((L,(L,b,b),b),(L,(L,b,b),b)) is M2( the carrier of L)
(L,(L,b,(L,b,b)),(L,(L,b,b),b)) is M2( the carrier of L)
the of L . ((L,b,(L,b,b)),(L,(L,b,b),b)) is M2( the carrier of L)