theorem :: GATE_2:2
for a, b, c, d being set holds
( not AND3 ((AND2 (a,d)),(AND2 (b,d)),(AND2 (c,d))) is empty iff not AND2 ((AND3 (a,b,c)),d) is empty )