theorem :: GATE_1:8

for a being set holds
( not XOR2 (a,{}) is empty iff not a is empty ) ;