theorem :: GATE_1:20

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