theorem :: GATE_1:2

for a being set holds
( not NOT1 a is empty iff a is empty ) ;