theorem Th14: :: BVFUNC25:13

for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'xor' ('not' a) = I_el Y