let x, y, z be Element of BOOLEAN ; :: thesis: inv1 . <*(xor2 . <*(xor2c . <*x,y*>),z*>)*> = xor2c . <*(xor2c . <*x,y*>),z*>
thus inv1 . <*(xor2 . <*(xor2c . <*x,y*>),z*>)*> = inv1 . <*(xor2 . <*(x 'xor' ('not' y)),z*>)*> by Def4
.= inv1 . <*((x 'xor' ('not' y)) 'xor' z)*> by FACIRC_1:def 4
.= 'not' ((x 'xor' ('not' y)) 'xor' z) by Def1
.= (x 'xor' ('not' y)) 'xor' ('not' z) by XBOOLEAN:74
.= xor2c . <*(x 'xor' ('not' y)),z*> by Def4
.= xor2c . <*(xor2c . <*x,y*>),z*> by Def4 ; :: thesis: verum