theorem :: GATE_1:1

( NOT1 {{}} = {} & NOT1 {} = {{}} ) by Def1;