:: YELLOW_5 semantic presentation

K88() is set

K19(K88()) is set

1 is set

L is non empty reflexive antisymmetric with_suprema RelStr

the U1 of L is set

a is M2( the U1 of L)

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

L is non empty reflexive antisymmetric with_infima RelStr

the U1 of L is set

a is M2( the U1 of L)

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

L is non empty transitive antisymmetric with_suprema RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

a "\/" b is M2( the U1 of L)

c is M2( the U1 of L)

L is non empty transitive antisymmetric with_infima RelStr

the U1 of L is set

c is M2( the U1 of L)

a is M2( the U1 of L)

b is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

L is non empty transitive antisymmetric with_suprema with_infima RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

c is M2( the U1 of L)

a "\/" c is M2( the U1 of L)

L is non empty transitive antisymmetric with_infima RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

c is M2( the U1 of L)

a "/\" c is M2( the U1 of L)

b "/\" c is M2( the U1 of L)

L is non empty transitive antisymmetric with_suprema RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

c is M2( the U1 of L)

a "\/" c is M2( the U1 of L)

b "\/" c is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

a "\/" b is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema RelStr

the U1 of L is set

a is M2( the U1 of L)

c is M2( the U1 of L)

b is M2( the U1 of L)

a "\/" b is M2( the U1 of L)

c "\/" b is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_infima RelStr

the U1 of L is set

b is M2( the U1 of L)

a is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

'not' a is M2( the U1 of L)

c is M2( the U1 of L)

'not' c is M2( the U1 of L)

'not' ('not' c) is M2( the U1 of L)

a "/\" ('not' a) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

a "\/" ('not' a) is M2( the U1 of L)

Top L is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

b "/\" ('not' a) is M2( the U1 of L)

(a "\/" ('not' a)) "/\" b is M2( the U1 of L)

(a "/\" b) "\/" (b "/\" ('not' a)) is M2( the U1 of L)

a "\/" b is M2( the U1 of L)

(a "\/" b) "/\" ('not' a) is M2( the U1 of L)

(a "/\" ('not' a)) "\/" (b "/\" ('not' a)) is M2( the U1 of L)

L is non empty RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

L is non empty RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

(L,b,a) is M2( the U1 of L)

'not' a is M2( the U1 of L)

b "/\" ('not' a) is M2( the U1 of L)

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

L is non empty antisymmetric with_suprema with_infima RelStr

the U1 of L is set

c is M2( the U1 of L)

d is M2( the U1 of L)

(L,c,d) is M2( the U1 of L)

(L,c,d) is M2( the U1 of L)

'not' d is M2( the U1 of L)

c "/\" ('not' d) is M2( the U1 of L)

(L,d,c) is M2( the U1 of L)

'not' c is M2( the U1 of L)

d "/\" ('not' c) is M2( the U1 of L)

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

(L,d,c) is M2( the U1 of L)

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

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

L is non empty RelStr

the U1 of L is set

L is non empty RelStr

the U1 of L is set

L is non empty antisymmetric with_infima RelStr

the U1 of L is set

L is non empty antisymmetric with_infima RelStr

the U1 of L is set

c is M2( the U1 of L)

d is M2( the U1 of L)

c "/\" d is M2( the U1 of L)

Bottom L is M2( the U1 of L)

d "/\" c is M2( the U1 of L)

L is non empty transitive antisymmetric with_suprema with_infima RelStr

the U1 of L is set

a is M2( the U1 of L)

c is M2( the U1 of L)

b is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

L is non empty transitive antisymmetric with_suprema with_infima RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

c is M2( the U1 of L)

(L,a,c) is M2( the U1 of L)

'not' c is M2( the U1 of L)

a "/\" ('not' c) is M2( the U1 of L)

(L,b,c) is M2( the U1 of L)

b "/\" ('not' c) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

c is M2( the U1 of L)

(L,b,a) is M2( the U1 of L)

'not' a is M2( the U1 of L)

b "/\" ('not' a) is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

the U1 of L is set

Bottom L is M2( the U1 of L)

a is M2( the U1 of L)

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

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

L is non empty transitive antisymmetric with_infima RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

c is M2( the U1 of L)

a "/\" c is M2( the U1 of L)

(a "/\" b) "\/" (a "/\" c) is M2( the U1 of L)

b "\/" c is M2( the U1 of L)

(b "\/" c) "/\" a is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

c is M2( the U1 of L)

b "/\" c is M2( the U1 of L)

a "\/" (b "/\" c) is M2( the U1 of L)

a "\/" b is M2( the U1 of L)

a "\/" c is M2( the U1 of L)

(a "\/" b) "/\" (a "\/" c) is M2( the U1 of L)

(a "\/" b) "/\" a is M2( the U1 of L)

(a "\/" b) "/\" c is M2( the U1 of L)

((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" c) is M2( the U1 of L)

a "\/" ((a "\/" b) "/\" c) is M2( the U1 of L)

c "/\" a is M2( the U1 of L)

c "/\" b is M2( the U1 of L)

(c "/\" a) "\/" (c "/\" b) is M2( the U1 of L)

a "\/" ((c "/\" a) "\/" (c "/\" b)) is M2( the U1 of L)

a "\/" (c "/\" a) is M2( the U1 of L)

(a "\/" (c "/\" a)) "\/" (c "/\" b) is M2( the U1 of L)

a "\/" (c "/\" b) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

a "\/" b is M2( the U1 of L)

c is M2( the U1 of L)

(L,(a "\/" b),c) is M2( the U1 of L)

'not' c is M2( the U1 of L)

(a "\/" b) "/\" ('not' c) is M2( the U1 of L)

(L,a,c) is M2( the U1 of L)

a "/\" ('not' c) is M2( the U1 of L)

(L,b,c) is M2( the U1 of L)

b "/\" ('not' c) is M2( the U1 of L)

(L,a,c) "\/" (L,b,c) is M2( the U1 of L)

(a "\/" b) "/\" ('not' c) is M2( the U1 of L)

('not' c) "/\" a is M2( the U1 of L)

('not' c) "/\" b is M2( the U1 of L)

(('not' c) "/\" a) "\/" (('not' c) "/\" b) is M2( the U1 of L)

L is non empty antisymmetric lower-bounded RelStr

the U1 of L is set

Bottom L is M2( the U1 of L)

a is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_infima lower-bounded RelStr

the U1 of L is set

Bottom L is M2( the U1 of L)

a is M2( the U1 of L)

b is M2( the U1 of L)

c is M2( the U1 of L)

b "/\" c is M2( the U1 of L)

a "/\" c is M2( the U1 of L)

L is non empty antisymmetric with_suprema lower-bounded RelStr

the U1 of L is set

Bottom L is M2( the U1 of L)

a is M2( the U1 of L)

b is M2( the U1 of L)

a "\/" b is M2( the U1 of L)

L is non empty transitive antisymmetric with_infima lower-bounded RelStr

the U1 of L is set

Bottom L is M2( the U1 of L)

a is M2( the U1 of L)

b is M2( the U1 of L)

c is M2( the U1 of L)

b "/\" c is M2( the U1 of L)

a "/\" c is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_infima lower-bounded RelStr

the U1 of L is set

Bottom L is M2( the U1 of L)

a is M2( the U1 of L)

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

'not' a is M2( the U1 of L)

(Bottom L) "/\" ('not' a) is M2( the U1 of L)

(Bottom L) "/\" ('not' a) is M2( the U1 of L)

L is non empty transitive antisymmetric with_infima lower-bounded RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

c is M2( the U1 of L)

Bottom L is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

a "/\" c is M2( the U1 of L)

L is non empty antisymmetric with_infima lower-bounded RelStr

the U1 of L is set

Bottom L is M2( the U1 of L)

a is M2( the U1 of L)

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

L is non empty transitive antisymmetric with_suprema with_infima lower-bounded RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

c is M2( the U1 of L)

b "/\" c is M2( the U1 of L)

a "/\" (b "/\" c) is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

(a "/\" b) "/\" c is M2( the U1 of L)

Bottom L is M2( the U1 of L)

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

L is non empty transitive antisymmetric with_suprema with_infima lower-bounded RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

c is M2( the U1 of L)

(L,b,c) is M2( the U1 of L)

'not' c is M2( the U1 of L)

b "/\" ('not' c) is M2( the U1 of L)

a "/\" (L,b,c) is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

(a "/\" b) "/\" ('not' c) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

(Bottom L) "/\" ('not' c) is M2( the U1 of L)

L is non empty transitive antisymmetric with_infima lower-bounded RelStr

the U1 of L is set

Bottom L is M2( the U1 of L)

a is M2( the U1 of L)

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

L is non empty transitive antisymmetric with_infima lower-bounded RelStr

the U1 of L is set

a is M2( the U1 of L)

c is M2( the U1 of L)

b is M2( the U1 of L)

a "/\" c is M2( the U1 of L)

Bottom L is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

L is non empty transitive antisymmetric with_infima lower-bounded RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

c is M2( the U1 of L)

b "/\" c is M2( the U1 of L)

a "/\" (b "/\" c) is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

(a "/\" b) "/\" c is M2( the U1 of L)

Bottom L is M2( the U1 of L)

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

a "/\" (b "/\" c) is M2( the U1 of L)

a "/\" c is M2( the U1 of L)

(a "/\" c) "/\" b is M2( the U1 of L)

Bottom L is M2( the U1 of L)

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded RelStr

the U1 of L is set

Bottom L is M2( the U1 of L)

a is M2( the U1 of L)

b is M2( the U1 of L)

c is M2( the U1 of L)

b "/\" c is M2( the U1 of L)

a "/\" c is M2( the U1 of L)

L is non empty transitive antisymmetric with_infima lower-bounded RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

c is M2( the U1 of L)

a "/\" c is M2( the U1 of L)

b "/\" c is M2( the U1 of L)

(a "/\" c) "/\" (b "/\" c) is M2( the U1 of L)

a "/\" (b "/\" c) is M2( the U1 of L)

c "/\" (a "/\" (b "/\" c)) is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

c "/\" (a "/\" b) is M2( the U1 of L)

(c "/\" (a "/\" b)) "/\" c is M2( the U1 of L)

Bottom L is M2( the U1 of L)

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

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

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

a "\/" b is M2( the U1 of L)

c is M2( the U1 of L)

b "/\" c is M2( the U1 of L)

(a "/\" b) "\/" (b "/\" c) is M2( the U1 of L)

c "/\" a is M2( the U1 of L)

((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) is M2( the U1 of L)

b "\/" c is M2( the U1 of L)

(a "\/" b) "/\" (b "\/" c) is M2( the U1 of L)

c "\/" a is M2( the U1 of L)

((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) is M2( the U1 of L)

a "\/" (b "/\" c) is M2( the U1 of L)

b "\/" (b "/\" c) is M2( the U1 of L)

(a "\/" (b "/\" c)) "/\" (b "\/" (b "/\" c)) is M2( the U1 of L)

((a "\/" (b "/\" c)) "/\" (b "\/" (b "/\" c))) "\/" (c "/\" a) is M2( the U1 of L)

(a "\/" (b "/\" c)) "/\" b is M2( the U1 of L)

((a "\/" (b "/\" c)) "/\" b) "\/" (c "/\" a) is M2( the U1 of L)

(a "\/" (b "/\" c)) "\/" (c "/\" a) is M2( the U1 of L)

b "\/" (c "/\" a) is M2( the U1 of L)

((a "\/" (b "/\" c)) "\/" (c "/\" a)) "/\" (b "\/" (c "/\" a)) is M2( the U1 of L)

b "\/" a is M2( the U1 of L)

(b "\/" c) "/\" (b "\/" a) is M2( the U1 of L)

((a "\/" (b "/\" c)) "\/" (c "/\" a)) "/\" ((b "\/" c) "/\" (b "\/" a)) is M2( the U1 of L)

a "\/" (c "/\" a) is M2( the U1 of L)

(b "/\" c) "\/" (a "\/" (c "/\" a)) is M2( the U1 of L)

((b "/\" c) "\/" (a "\/" (c "/\" a))) "/\" ((b "\/" c) "/\" (b "\/" a)) is M2( the U1 of L)

(b "/\" c) "\/" a is M2( the U1 of L)

((b "/\" c) "\/" a) "/\" ((b "\/" c) "/\" (b "\/" a)) is M2( the U1 of L)

(b "\/" a) "/\" (c "\/" a) is M2( the U1 of L)

((b "\/" a) "/\" (c "\/" a)) "/\" ((b "\/" c) "/\" (b "\/" a)) is M2( the U1 of L)

(c "\/" a) "/\" (b "\/" a) is M2( the U1 of L)

((c "\/" a) "/\" (b "\/" a)) "/\" (b "\/" c) is M2( the U1 of L)

(b "\/" a) "/\" (((c "\/" a) "/\" (b "\/" a)) "/\" (b "\/" c)) is M2( the U1 of L)

(c "\/" a) "/\" (b "\/" c) is M2( the U1 of L)

(b "\/" a) "/\" ((c "\/" a) "/\" (b "\/" c)) is M2( the U1 of L)

(b "\/" a) "/\" ((b "\/" a) "/\" ((c "\/" a) "/\" (b "\/" c))) is M2( the U1 of L)

(b "\/" a) "/\" (b "\/" a) is M2( the U1 of L)

((b "\/" a) "/\" (b "\/" a)) "/\" ((c "\/" a) "/\" (b "\/" c)) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

Bottom L is M2( the U1 of L)

Top L is M2( the U1 of L)

a is M2( the U1 of L)

'not' a is M2( the U1 of L)

a "/\" ('not' a) is M2( the U1 of L)

a "\/" ('not' a) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

c is M2( the U1 of L)

b "\/" c is M2( the U1 of L)

a "\/" b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

(a "/\" ('not' b)) "\/" b is M2( the U1 of L)

c "\/" b is M2( the U1 of L)

b "\/" a is M2( the U1 of L)

b "\/" ('not' b) is M2( the U1 of L)

(b "\/" a) "/\" (b "\/" ('not' b)) is M2( the U1 of L)

Top L is M2( the U1 of L)

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

'not' a is M2( the U1 of L)

b is M2( the U1 of L)

a "\/" b is M2( the U1 of L)

'not' (a "\/" b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

('not' a) "/\" ('not' b) is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

'not' (a "/\" b) is M2( the U1 of L)

('not' a) "\/" ('not' b) is M2( the U1 of L)

(a "\/" b) "/\" (('not' a) "/\" ('not' b)) is M2( the U1 of L)

(a "\/" b) "/\" ('not' a) is M2( the U1 of L)

((a "\/" b) "/\" ('not' a)) "/\" ('not' b) is M2( the U1 of L)

('not' a) "/\" a is M2( the U1 of L)

('not' a) "/\" b is M2( the U1 of L)

(('not' a) "/\" a) "\/" (('not' a) "/\" b) is M2( the U1 of L)

((('not' a) "/\" a) "\/" (('not' a) "/\" b)) "/\" ('not' b) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

(Bottom L) "\/" (('not' a) "/\" b) is M2( the U1 of L)

((Bottom L) "\/" (('not' a) "/\" b)) "/\" ('not' b) is M2( the U1 of L)

(('not' a) "/\" b) "/\" ('not' b) is M2( the U1 of L)

b "/\" ('not' b) is M2( the U1 of L)

('not' a) "/\" (b "/\" ('not' b)) is M2( the U1 of L)

('not' a) "/\" (Bottom L) is M2( the U1 of L)

(a "\/" b) "\/" (('not' a) "/\" ('not' b)) is M2( the U1 of L)

b "\/" (('not' a) "/\" ('not' b)) is M2( the U1 of L)

a "\/" (b "\/" (('not' a) "/\" ('not' b))) is M2( the U1 of L)

b "\/" ('not' a) is M2( the U1 of L)

b "\/" ('not' b) is M2( the U1 of L)

(b "\/" ('not' a)) "/\" (b "\/" ('not' b)) is M2( the U1 of L)

a "\/" ((b "\/" ('not' a)) "/\" (b "\/" ('not' b))) is M2( the U1 of L)

Top L is M2( the U1 of L)

(b "\/" ('not' a)) "/\" (Top L) is M2( the U1 of L)

a "\/" ((b "\/" ('not' a)) "/\" (Top L)) is M2( the U1 of L)

a "\/" (b "\/" ('not' a)) is M2( the U1 of L)

a "\/" ('not' a) is M2( the U1 of L)

(a "\/" ('not' a)) "\/" b is M2( the U1 of L)

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

(a "/\" b) "/\" (('not' a) "\/" ('not' b)) is M2( the U1 of L)

b "/\" (('not' a) "\/" ('not' b)) is M2( the U1 of L)

a "/\" (b "/\" (('not' a) "\/" ('not' b))) is M2( the U1 of L)

b "/\" ('not' a) is M2( the U1 of L)

(b "/\" ('not' a)) "\/" (b "/\" ('not' b)) is M2( the U1 of L)

a "/\" ((b "/\" ('not' a)) "\/" (b "/\" ('not' b))) is M2( the U1 of L)

(b "/\" ('not' a)) "\/" (Bottom L) is M2( the U1 of L)

a "/\" ((b "/\" ('not' a)) "\/" (Bottom L)) is M2( the U1 of L)

a "/\" (b "/\" ('not' a)) is M2( the U1 of L)

a "/\" ('not' a) is M2( the U1 of L)

(a "/\" ('not' a)) "/\" b is M2( the U1 of L)

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

(a "/\" b) "\/" (('not' a) "\/" ('not' b)) is M2( the U1 of L)

(a "/\" b) "\/" ('not' a) is M2( the U1 of L)

((a "/\" b) "\/" ('not' a)) "\/" ('not' b) is M2( the U1 of L)

('not' a) "\/" a is M2( the U1 of L)

('not' a) "\/" b is M2( the U1 of L)

(('not' a) "\/" a) "/\" (('not' a) "\/" b) is M2( the U1 of L)

((('not' a) "\/" a) "/\" (('not' a) "\/" b)) "\/" ('not' b) is M2( the U1 of L)

(Top L) "/\" (('not' a) "\/" b) is M2( the U1 of L)

((Top L) "/\" (('not' a) "\/" b)) "\/" ('not' b) is M2( the U1 of L)

(('not' a) "\/" b) "\/" ('not' b) is M2( the U1 of L)

('not' a) "\/" (b "\/" ('not' b)) is M2( the U1 of L)

('not' a) "\/" (Top L) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

'not' a is M2( the U1 of L)

b is M2( the U1 of L)

'not' b is M2( the U1 of L)

b "/\" a is M2( the U1 of L)

'not' (b "/\" a) is M2( the U1 of L)

('not' b) "\/" ('not' a) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

c is M2( the U1 of L)

(L,c,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

c "/\" ('not' b) is M2( the U1 of L)

(L,c,a) is M2( the U1 of L)

'not' a is M2( the U1 of L)

c "/\" ('not' a) is M2( the U1 of L)

c "/\" ('not' b) is M2( the U1 of L)

c "/\" ('not' a) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

c is M2( the U1 of L)

(L,b,c) is M2( the U1 of L)

'not' c is M2( the U1 of L)

b "/\" ('not' c) is M2( the U1 of L)

d is M2( the U1 of L)

(L,a,d) is M2( the U1 of L)

'not' d is M2( the U1 of L)

a "/\" ('not' d) is M2( the U1 of L)

a "/\" ('not' d) is M2( the U1 of L)

a "/\" ('not' c) is M2( the U1 of L)

b "/\" ('not' c) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

c is M2( the U1 of L)

b "\/" c is M2( the U1 of L)

(L,a,c) is M2( the U1 of L)

'not' c is M2( the U1 of L)

a "/\" ('not' c) is M2( the U1 of L)

(b "\/" c) "/\" ('not' b) is M2( the U1 of L)

('not' b) "/\" b is M2( the U1 of L)

('not' b) "/\" c is M2( the U1 of L)

(('not' b) "/\" b) "\/" (('not' b) "/\" c) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

(Bottom L) "\/" (('not' b) "/\" c) is M2( the U1 of L)

c "/\" ('not' b) is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

(b "\/" c) "/\" ('not' c) is M2( the U1 of L)

('not' c) "/\" b is M2( the U1 of L)

('not' c) "/\" c is M2( the U1 of L)

(('not' c) "/\" b) "\/" (('not' c) "/\" c) is M2( the U1 of L)

(('not' c) "/\" b) "\/" (Bottom L) is M2( the U1 of L)

a "/\" ('not' c) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

'not' a is M2( the U1 of L)

b is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

'not' (a "/\" b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

('not' a) "\/" ('not' b) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

'not' a is M2( the U1 of L)

b is M2( the U1 of L)

a "\/" b is M2( the U1 of L)

'not' (a "\/" b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

('not' a) "/\" ('not' b) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

Bottom L is M2( the U1 of L)

a is M2( the U1 of L)

b is M2( the U1 of L)

(L,b,a) is M2( the U1 of L)

'not' a is M2( the U1 of L)

b "/\" ('not' a) is M2( the U1 of L)

b "/\" ('not' a) is M2( the U1 of L)

(b "/\" ('not' a)) "/\" a is M2( the U1 of L)

('not' a) "/\" a is M2( the U1 of L)

b "/\" (('not' a) "/\" a) is M2( the U1 of L)

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

(L,b,a) is M2( the U1 of L)

'not' a is M2( the U1 of L)

b "/\" ('not' a) is M2( the U1 of L)

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

a "\/" b is M2( the U1 of L)

a "\/" ('not' a) is M2( the U1 of L)

(a "\/" b) "/\" (a "\/" ('not' a)) is M2( the U1 of L)

('not' a) "\/" a is M2( the U1 of L)

b "/\" (('not' a) "\/" a) is M2( the U1 of L)

Top L is M2( the U1 of L)

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

Bottom L is M2( the U1 of L)

a is M2( the U1 of L)

b is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

b "\/" a is M2( the U1 of L)

b "\/" ('not' b) is M2( the U1 of L)

(b "\/" a) "/\" (b "\/" ('not' b)) is M2( the U1 of L)

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

a "\/" b is M2( the U1 of L)

Top L is M2( the U1 of L)

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

a "/\" ('not' b) is M2( the U1 of L)

b "/\" ('not' b) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

Bottom L is M2( the U1 of L)

a is M2( the U1 of L)

b is M2( the U1 of L)

c is M2( the U1 of L)

b "\/" c is M2( the U1 of L)

a "/\" c is M2( the U1 of L)

a "/\" (b "\/" c) is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

a "\/" b is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

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

b "\/" a is M2( the U1 of L)

b "\/" ('not' b) is M2( the U1 of L)

(b "\/" a) "/\" (b "\/" ('not' b)) is M2( the U1 of L)

Top L is M2( the U1 of L)

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

Bottom L is M2( the U1 of L)

a is M2( the U1 of L)

b is M2( the U1 of L)

a "\/" b is M2( the U1 of L)

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

'not' (a "\/" b) is M2( the U1 of L)

a "/\" ('not' (a "\/" b)) is M2( the U1 of L)

'not' a is M2( the U1 of L)

'not' b is M2( the U1 of L)

('not' a) "/\" ('not' b) is M2( the U1 of L)

a "/\" (('not' a) "/\" ('not' b)) is M2( the U1 of L)

a "/\" ('not' a) is M2( the U1 of L)

(a "/\" ('not' a)) "/\" ('not' b) is M2( the U1 of L)

(Bottom L) "/\" ('not' b) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

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

'not' (a "/\" b) is M2( the U1 of L)

a "/\" ('not' (a "/\" b)) is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

'not' a is M2( the U1 of L)

('not' a) "\/" ('not' b) is M2( the U1 of L)

a "/\" (('not' a) "\/" ('not' b)) is M2( the U1 of L)

a "/\" ('not' a) is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

(a "/\" ('not' a)) "\/" (a "/\" ('not' b)) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

(Bottom L) "\/" (a "/\" ('not' b)) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

Bottom L is M2( the U1 of L)

a is M2( the U1 of L)

b is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

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

('not' b) "/\" b is M2( the U1 of L)

a "/\" (('not' b) "/\" b) is M2( the U1 of L)

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

(L,b,a) is M2( the U1 of L)

'not' a is M2( the U1 of L)

b "/\" ('not' a) is M2( the U1 of L)

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

a "\/" b is M2( the U1 of L)

a "\/" ('not' a) is M2( the U1 of L)

(a "\/" b) "/\" (a "\/" ('not' a)) is M2( the U1 of L)

Top L is M2( the U1 of L)

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

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

(a "/\" b) "\/" a is M2( the U1 of L)

(a "/\" b) "\/" ('not' b) is M2( the U1 of L)

((a "/\" b) "\/" a) "/\" ((a "/\" b) "\/" ('not' b)) is M2( the U1 of L)

a "/\" ((a "/\" b) "\/" ('not' b)) is M2( the U1 of L)

('not' b) "\/" a is M2( the U1 of L)

('not' b) "\/" b is M2( the U1 of L)

(('not' b) "\/" a) "/\" (('not' b) "\/" b) is M2( the U1 of L)

a "/\" ((('not' b) "\/" a) "/\" (('not' b) "\/" b)) is M2( the U1 of L)

Top L is M2( the U1 of L)

(('not' b) "\/" a) "/\" (Top L) is M2( the U1 of L)

a "/\" ((('not' b) "\/" a) "/\" (Top L)) is M2( the U1 of L)

a "/\" (('not' b) "\/" a) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

c is M2( the U1 of L)

(L,b,c) is M2( the U1 of L)

'not' c is M2( the U1 of L)

b "/\" ('not' c) is M2( the U1 of L)

(L,a,(L,b,c)) is M2( the U1 of L)

'not' (L,b,c) is M2( the U1 of L)

a "/\" ('not' (L,b,c)) is M2( the U1 of L)

a "/\" c is M2( the U1 of L)

(L,a,b) "\/" (a "/\" c) is M2( the U1 of L)

'not' ('not' c) is M2( the U1 of L)

('not' b) "\/" ('not' ('not' c)) is M2( the U1 of L)

a "/\" (('not' b) "\/" ('not' ('not' c))) is M2( the U1 of L)

('not' b) "\/" c is M2( the U1 of L)

a "/\" (('not' b) "\/" c) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

(L,a,(L,a,b)) is M2( the U1 of L)

'not' (L,a,b) is M2( the U1 of L)

a "/\" ('not' (L,a,b)) is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

'not' a is M2( the U1 of L)

'not' ('not' b) is M2( the U1 of L)

('not' a) "\/" ('not' ('not' b)) is M2( the U1 of L)

a "/\" (('not' a) "\/" ('not' ('not' b))) is M2( the U1 of L)

('not' a) "\/" b is M2( the U1 of L)

a "/\" (('not' a) "\/" b) is M2( the U1 of L)

a "/\" ('not' a) is M2( the U1 of L)

(a "/\" ('not' a)) "\/" (a "/\" b) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

a "\/" b is M2( the U1 of L)

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

'not' b is M2( the U1 of L)

(a "\/" b) "/\" ('not' b) is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

(a "\/" b) "/\" ('not' b) is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

b "/\" ('not' b) is M2( the U1 of L)

(a "/\" ('not' b)) "\/" (b "/\" ('not' b)) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

(a "/\" ('not' b)) "\/" (Bottom L) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

Bottom L is M2( the U1 of L)

a is M2( the U1 of L)

b is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

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

a "/\" ('not' b) is M2( the U1 of L)

'not' a is M2( the U1 of L)

'not' ('not' b) is M2( the U1 of L)

('not' a) "\/" ('not' ('not' b)) is M2( the U1 of L)

('not' a) "\/" b is M2( the U1 of L)

a "/\" (('not' a) "\/" b) is M2( the U1 of L)

a "/\" ('not' a) is M2( the U1 of L)

(a "/\" ('not' a)) "\/" (a "/\" b) is M2( the U1 of L)

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

c is M2( the U1 of L)

b "\/" c is M2( the U1 of L)

(L,a,(b "\/" c)) is M2( the U1 of L)

'not' (b "\/" c) is M2( the U1 of L)

a "/\" ('not' (b "\/" c)) is M2( the U1 of L)

(L,a,c) is M2( the U1 of L)

'not' c is M2( the U1 of L)

a "/\" ('not' c) is M2( the U1 of L)

(L,a,b) "/\" (L,a,c) is M2( the U1 of L)

('not' b) "/\" ('not' c) is M2( the U1 of L)

a "/\" (('not' b) "/\" ('not' c)) is M2( the U1 of L)

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

(a "/\" a) "/\" (('not' b) "/\" ('not' c)) is M2( the U1 of L)

(a "/\" a) "/\" ('not' b) is M2( the U1 of L)

((a "/\" a) "/\" ('not' b)) "/\" ('not' c) is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

a "/\" (a "/\" ('not' b)) is M2( the U1 of L)

(a "/\" (a "/\" ('not' b))) "/\" ('not' c) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

c is M2( the U1 of L)

b "/\" c is M2( the U1 of L)

(L,a,(b "/\" c)) is M2( the U1 of L)

'not' (b "/\" c) is M2( the U1 of L)

a "/\" ('not' (b "/\" c)) is M2( the U1 of L)

(L,a,c) is M2( the U1 of L)

'not' c is M2( the U1 of L)

a "/\" ('not' c) is M2( the U1 of L)

(L,a,b) "\/" (L,a,c) is M2( the U1 of L)

('not' b) "\/" ('not' c) is M2( the U1 of L)

a "/\" (('not' b) "\/" ('not' c)) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

c is M2( the U1 of L)

(L,b,c) is M2( the U1 of L)

'not' c is M2( the U1 of L)

b "/\" ('not' c) is M2( the U1 of L)

a "/\" (L,b,c) is M2( the U1 of L)

a "/\" c is M2( the U1 of L)

(L,(a "/\" b),(a "/\" c)) is M2( the U1 of L)

'not' (a "/\" c) is M2( the U1 of L)

(a "/\" b) "/\" ('not' (a "/\" c)) is M2( the U1 of L)

'not' a is M2( the U1 of L)

('not' a) "\/" ('not' c) is M2( the U1 of L)

(a "/\" b) "/\" (('not' a) "\/" ('not' c)) is M2( the U1 of L)

(a "/\" b) "/\" ('not' a) is M2( the U1 of L)

(a "/\" b) "/\" ('not' c) is M2( the U1 of L)

((a "/\" b) "/\" ('not' a)) "\/" ((a "/\" b) "/\" ('not' c)) is M2( the U1 of L)

a "/\" ('not' a) is M2( the U1 of L)

(a "/\" ('not' a)) "/\" b is M2( the U1 of L)

((a "/\" ('not' a)) "/\" b) "\/" ((a "/\" b) "/\" ('not' c)) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

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

((Bottom L) "/\" b) "\/" ((a "/\" b) "/\" ('not' c)) is M2( the U1 of L)

(Bottom L) "\/" ((a "/\" b) "/\" ('not' c)) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

a "\/" b is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

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

'not' (a "/\" b) is M2( the U1 of L)

(a "\/" b) "/\" ('not' (a "/\" b)) is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

(L,b,a) is M2( the U1 of L)

'not' a is M2( the U1 of L)

b "/\" ('not' a) is M2( the U1 of L)

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

('not' a) "\/" ('not' b) is M2( the U1 of L)

(a "\/" b) "/\" (('not' a) "\/" ('not' b)) is M2( the U1 of L)

(a "\/" b) "/\" ('not' a) is M2( the U1 of L)

(a "\/" b) "/\" ('not' b) is M2( the U1 of L)

((a "\/" b) "/\" ('not' a)) "\/" ((a "\/" b) "/\" ('not' b)) is M2( the U1 of L)

a "/\" ('not' a) is M2( the U1 of L)

b "/\" ('not' a) is M2( the U1 of L)

(a "/\" ('not' a)) "\/" (b "/\" ('not' a)) is M2( the U1 of L)

((a "/\" ('not' a)) "\/" (b "/\" ('not' a))) "\/" ((a "\/" b) "/\" ('not' b)) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

(Bottom L) "\/" (b "/\" ('not' a)) is M2( the U1 of L)

((Bottom L) "\/" (b "/\" ('not' a))) "\/" ((a "\/" b) "/\" ('not' b)) is M2( the U1 of L)

(L,b,a) "\/" ((a "\/" b) "/\" ('not' b)) is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

b "/\" ('not' b) is M2( the U1 of L)

(a "/\" ('not' b)) "\/" (b "/\" ('not' b)) is M2( the U1 of L)

(L,b,a) "\/" ((a "/\" ('not' b)) "\/" (b "/\" ('not' b))) is M2( the U1 of L)

(a "/\" ('not' b)) "\/" (Bottom L) is M2( the U1 of L)

(L,b,a) "\/" ((a "/\" ('not' b)) "\/" (Bottom L)) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

c is M2( the U1 of L)

(L,(L,a,b),c) is M2( the U1 of L)

'not' c is M2( the U1 of L)

(L,a,b) "/\" ('not' c) is M2( the U1 of L)

b "\/" c is M2( the U1 of L)

(L,a,(b "\/" c)) is M2( the U1 of L)

'not' (b "\/" c) is M2( the U1 of L)

a "/\" ('not' (b "\/" c)) is M2( the U1 of L)

('not' b) "/\" ('not' c) is M2( the U1 of L)

a "/\" (('not' b) "/\" ('not' c)) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

Bottom L is M2( the U1 of L)

the U1 of L is set

'not' (Bottom L) is M2( the U1 of L)

Top L is M2( the U1 of L)

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

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

Top L is M2( the U1 of L)

the U1 of L is set

'not' (Top L) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

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

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

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

'not' a is M2( the U1 of L)

a "/\" ('not' a) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

Bottom L is M2( the U1 of L)

a is M2( the U1 of L)

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

'not' (Bottom L) is M2( the U1 of L)

a "/\" ('not' (Bottom L)) is M2( the U1 of L)

Top L is M2( the U1 of L)

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

'not' a is M2( the U1 of L)

b is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

'not' (L,a,b) is M2( the U1 of L)

('not' a) "\/" b is M2( the U1 of L)

'not' ('not' b) is M2( the U1 of L)

('not' a) "\/" ('not' ('not' b)) is M2( the U1 of L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

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

(a "/\" b) "/\" ('not' b) is M2( the U1 of L)

((a "/\" b) "/\" ('not' b)) "/\" a is M2( the U1 of L)

b "/\" ('not' b) is M2( the U1 of L)

a "/\" (b "/\" ('not' b)) is M2( the U1 of L)

(a "/\" (b "/\" ('not' b))) "/\" a is M2( the U1 of L)

Bottom L is M2( the U1 of L)

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

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

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

(L,a,b) is M2( the U1 of L)

'not' b is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

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

('not' b) "/\" b is M2( the U1 of L)

a "/\" (('not' b) "/\" b) is M2( the U1 of L)

Bottom L is M2( the U1 of L)

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V101() distributive V141() complemented Boolean RelStr

the U1 of L is set

a is M2( the U1 of L)

b is M2( the U1 of L)

a "\/" b is M2( the U1 of L)

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

'not' b is M2( the U1 of L)

(a "\/" b) "/\" ('not' b) is M2( the U1 of L)

a "/\" b is M2( the U1 of L)

Bottom L is M2( the U1 of L)

a "\/" ('not' b) is M2( the U1 of L)

b "\/" ('not' b) is M2( the U1 of L)

(a "\/" ('not' b)) "/\" (b "\/" ('not' b)) is M2( the U1 of L)

(Bottom L) "\/" ('not' b) is M2( the U1 of L)

Top L is M2( the U1 of L)

(a "\/" ('not' b)) "/\" (Top L) is M2( the U1 of L)

(a "\/" b) "/\" ('not' b) is M2( the U1 of L)

a "/\" ('not' b) is M2( the U1 of L)

b "/\" ('not' b) is M2( the U1 of L)

(a "/\" ('not' b)) "\/" (b "/\" ('not' b)) is M2( the U1 of L)

(a "/\" ('not' b)) "\/" (Bottom L) is M2( the U1 of L)