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

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)

(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 )

(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)

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)

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)

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)

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)

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)

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)

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)

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