let x, y be Element of BOOLEAN ; ( 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; ( 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
; ( 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
; ( 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
; ( and2c . <*0,1*> = 0 & and2c . <*1,0*> = 1 & and2c . <*1,1*> = 0 )
thus and2c . <*0,1*> =
FALSE '&' ('not' TRUE)
by Def3
.=
0
; ( and2c . <*1,0*> = 1 & and2c . <*1,1*> = 0 )
thus and2c . <*1,0*> =
TRUE '&' ('not' FALSE)
by Def3
.=
1
; and2c . <*1,1*> = 0
thus and2c . <*1,1*> =
TRUE '&' ('not' TRUE)
by Def3
.=
0
; verum