theorem :: GFACIRC1:9

for x, y, z being Element of BOOLEAN holds inv1 . <*(xor2c . <*(xor2b . <*x,y*>),z*>)*> = xor2 . <*(xor2 . <*x,y*>),z*>