:: deftheorem Def18 defines AND5 GATE_1:def 18 :
for a, b, c, d, e being set holds
( ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty implies AND5 (a,b,c,d,e) = NOT1 {} ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty ) implies AND5 (a,b,c,d,e) = {} ) );