let a be set ; :: thesis: XOR2 (a,a) is empty

( ( ( not a is empty & a is empty ) or ( a is empty & not a is empty ) ) iff not XOR2 (a,a) is empty ) ;

hence XOR2 (a,a) is empty ; :: thesis: verum

( ( ( not a is empty & a is empty ) or ( a is empty & not a is empty ) ) iff not XOR2 (a,a) is empty ) ;

hence XOR2 (a,a) is empty ; :: thesis: verum