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