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