let x, y be Element of BOOLEAN ; ( and2 . <*x,y*> = nor2b . <*x,y*> & and2a . <*x,y*> = nor2a . <*y,x*> & and2b . <*x,y*> = nor2 . <*x,y*> )
thus and2 . <*x,y*> =
'not' (('not' x) 'or' ('not' y))
by Def1
.=
nor2b . <*x,y*>
by Def12
; ( and2a . <*x,y*> = nor2a . <*y,x*> & and2b . <*x,y*> = nor2 . <*x,y*> )
thus and2a . <*x,y*> =
'not' (('not' ('not' x)) 'or' ('not' y))
by Def2
.=
nor2a . <*y,x*>
by Def11
; and2b . <*x,y*> = nor2 . <*x,y*>
thus and2b . <*x,y*> =
'not' (('not' ('not' x)) 'or' ('not' ('not' y)))
by Def3
.=
nor2 . <*x,y*>
by Def10
; verum