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