:: deftheorem defines <=> BVFUNC_1:def 19 :
for x, y being boolean object holds x <=> y = 'not' (x 'xor' y);