theorem :: GFACIRC1:3

for x, y being Element of BOOLEAN holds
( and2c . <*x,y*> = x '&' ('not' y) & and2c . <*x,y*> = and2a . <*y,x*> & and2c . <*x,y*> = nor2a . <*x,y*> & and2c . <*0,0*> = 0 & and2c . <*0,1*> = 0 & and2c . <*1,0*> = 1 & and2c . <*1,1*> = 0 )