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