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