theorem
for
a,
b,
c,
d,
e,
f,
g,
h being
set holds
( not
NAND8 (
a,
b,
c,
d,
e,
f,
g,
h) is
empty & not
a is
empty & not
b is
empty & not
c is
empty & not
d is
empty & not
e is
empty & not
f is
empty & not
g is
empty iff
h is
empty )
by Def32;