let a, b be set ; :: thesis: ( not EQV2 a,b is empty iff XOR2 a,b is empty )
( not EQV2 a,b is empty iff ( not a is empty iff not b is empty ) ) ;
hence ( not EQV2 a,b is empty iff XOR2 a,b is empty ) ; :: thesis: verum