:: deftheorem Def1 defines NOT1 GATE_1:def 1 :
for a being set holds
( ( not a is empty implies NOT1 a = {} ) & ( a is empty implies NOT1 a = {{}} ) );