for a, b being set holds
( not NOR2 (a,b) is empty iff ( a is empty & b is empty ) ) ;