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