for a, b being set holds
( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) iff not XOR2 (a,b) is empty ) ;