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