:: deftheorem Def4 defines xor2c GFACIRC1:def 4 :
for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = xor2c iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' ('not' y) );