let x, y be Element of BOOLEAN ; :: thesis: ( xor2c . <*x,y*> = x 'xor' ('not' y) & xor2c . <*x,y*> = xor2a . <*x,y*> & xor2c . <*x,y*> = or2 . <*(nor2 . <*x,y*>),(and2 . <*x,y*>)*> & xor2c . <*0,0*> = 1 & xor2c . <*0,1*> = 0 & xor2c . <*1,0*> = 0 & xor2c . <*1,1*> = 1 )
thus xor2c . <*x,y*> = x 'xor' ('not' y) by Def4; :: thesis: ( xor2c . <*x,y*> = xor2a . <*x,y*> & xor2c . <*x,y*> = or2 . <*(nor2 . <*x,y*>),(and2 . <*x,y*>)*> & xor2c . <*0,0*> = 1 & xor2c . <*0,1*> = 0 & xor2c . <*1,0*> = 0 & xor2c . <*1,1*> = 1 )
thus xor2c . <*x,y*> = x 'xor' ('not' y) by Def4
.= ('not' x) 'xor' y
.= xor2a . <*x,y*> by TWOSCOMP:def 14 ; :: thesis: ( xor2c . <*x,y*> = or2 . <*(nor2 . <*x,y*>),(and2 . <*x,y*>)*> & xor2c . <*0,0*> = 1 & xor2c . <*0,1*> = 0 & xor2c . <*1,0*> = 0 & xor2c . <*1,1*> = 1 )
thus xor2c . <*x,y*> = x 'xor' ('not' y) by Def4
.= (('not' x) '&' ('not' y)) 'or' (x '&' ('not' ('not' y)))
.= or2 . <*(('not' x) '&' ('not' y)),(x '&' y)*> by FACIRC_1:def 5
.= or2 . <*(nor2 . <*x,y*>),(x '&' y)*> by TWOSCOMP:54
.= or2 . <*(nor2 . <*x,y*>),(and2 . <*x,y*>)*> by FACIRC_1:def 6 ; :: thesis: ( xor2c . <*0,0*> = 1 & xor2c . <*0,1*> = 0 & xor2c . <*1,0*> = 0 & xor2c . <*1,1*> = 1 )
thus xor2c . <*0,0*> = FALSE 'xor' ('not' FALSE) by Def4
.= 1 by XBOOLEAN:102 ; :: thesis: ( xor2c . <*0,1*> = 0 & xor2c . <*1,0*> = 0 & xor2c . <*1,1*> = 1 )
thus xor2c . <*0,1*> = FALSE 'xor' ('not' TRUE) by Def4
.= 0 ; :: thesis: ( xor2c . <*1,0*> = 0 & xor2c . <*1,1*> = 1 )
thus xor2c . <*1,0*> = TRUE 'xor' ('not' FALSE) by Def4
.= 0 ; :: thesis: xor2c . <*1,1*> = 1
thus xor2c . <*1,1*> = TRUE 'xor' ('not' TRUE) by Def4
.= 1 by BINARITH:7 ; :: thesis: verum