:: deftheorem Def14 defines AND4 GATE_1:def 14 :
for a, b, c, d being set holds
( ( not a is empty & not b is empty & not c is empty & not d is empty implies AND4 (a,b,c,d) = NOT1 {} ) & ( ( a is empty or b is empty or c is empty or d is empty ) implies AND4 (a,b,c,d) = {} ) );