theorem :: GFACIRC1:8

for x, y, z being Element of BOOLEAN holds xor2c . <*(xor2a . <*x,y*>),z*> = xor2c . <*(xor2c . <*x,y*>),z*> by Th4;