theorem :: BVFUNC_1:59

for x, y being boolean object holds 'not' (x <=> y) = x 'xor' y ;