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