:: deftheorem Def7 defines NOR2 GATE_1:def 7 :
for a, b being set holds
( ( not a is empty or not b is empty or NOR2 (a,b) = NOT1 {} ) & ( ( not a is empty or not b is empty ) implies NOR2 (a,b) = {} ) );