let x, y be Element of BOOLEAN ; :: thesis: ( and2c . <*x,y*> = x '&' ('not' y) & and2c . <*x,y*> = and2a . <*y,x*> & and2c . <*x,y*> = nor2a . <*x,y*> & and2c . <*0 ,0 *> = 0 & and2c . <*0 ,1*> = 0 & and2c . <*1,0 *> = 1 & and2c . <*1,1*> = 0 )
thus and2c . <*x,y*> = x '&' ('not' y) by Def3; :: thesis: ( and2c . <*x,y*> = and2a . <*y,x*> & and2c . <*x,y*> = nor2a . <*x,y*> & and2c . <*0 ,0 *> = 0 & and2c . <*0 ,1*> = 0 & and2c . <*1,0 *> = 1 & and2c . <*1,1*> = 0 )
thus and2c . <*x,y*> = x '&' ('not' y) by Def3
.= and2a . <*y,x*> by TWOSCOMP:def 2 ; :: thesis: ( and2c . <*x,y*> = nor2a . <*x,y*> & and2c . <*0 ,0 *> = 0 & and2c . <*0 ,1*> = 0 & and2c . <*1,0 *> = 1 & and2c . <*1,1*> = 0 )
thus and2c . <*x,y*> = 'not' (('not' x) 'or' ('not' ('not' y))) by Def3
.= nor2a . <*x,y*> by TWOSCOMP:def 11 ; :: thesis: ( and2c . <*0 ,0 *> = 0 & and2c . <*0 ,1*> = 0 & and2c . <*1,0 *> = 1 & and2c . <*1,1*> = 0 )
thus and2c . <*0 ,0 *> = FALSE '&' ('not' FALSE ) by Def3
.= 0 ; :: thesis: ( and2c . <*0 ,1*> = 0 & and2c . <*1,0 *> = 1 & and2c . <*1,1*> = 0 )
thus and2c . <*0 ,1*> = FALSE '&' ('not' TRUE ) by Def3
.= 0 ; :: thesis: ( and2c . <*1,0 *> = 1 & and2c . <*1,1*> = 0 )
thus and2c . <*1,0 *> = TRUE '&' ('not' FALSE ) by Def3
.= 1 ; :: thesis: and2c . <*1,1*> = 0
thus and2c . <*1,1*> = TRUE '&' ('not' TRUE ) by Def3
.= 0 ; :: thesis: verum