let x, y be Element of BOOLEAN ; :: thesis: xor2b . <*x,y*> = xor2 . <*x,y*>
thus xor2b . <*x,y*> = ('not' x) 'xor' ('not' y) by Def8
.= x 'xor' y
.= xor2 . <*x,y*> by FACIRC_1:def 4 ; :: thesis: verum