theorem Th4: :: GFACIRC1:4

for x, y being Element of BOOLEAN holds
( xor2c . <*x,y*> = x 'xor' ('not' y) & xor2c . <*x,y*> = xor2a . <*x,y*> & xor2c . <*x,y*> = or2 . <*(nor2 . <*x,y*>),(and2 . <*x,y*>)*> & xor2c . <*0,0*> = 1 & xor2c . <*0,1*> = 0 & xor2c . <*1,0*> = 0 & xor2c . <*1,1*> = 1 )