:: deftheorem Def33 defines NOR8 GATE_1:def 33 :
for a, b, c, d, e, f, g, h being set holds
( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty or NOR8 (a,b,c,d,e,f,g,h) = NOT1 {} ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty ) implies NOR8 (a,b,c,d,e,f,g,h) = {} ) );