let x, y be Element of BOOLEAN ; :: thesis: and2a . <*x,y*> = nor2a . <*y,x*>
thus and2a . <*x,y*> = 'not' (('not' ('not' x)) 'or' ('not' y)) by Def1
.= nor2a . <*y,x*> by Def6 ; :: thesis: verum