theorem :: GATE_1:10

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