theorem :: GATE_1:22

for a, b, c, d being set holds
( not NAND4 (a,b,c,d) is empty & not a is empty & not b is empty & not c is empty iff d is empty ) by Def16;