let x, y be Element of BOOLEAN ; :: thesis: or2a . <*x,y*> = nand2a . <*y,x*>
thus or2a . <*x,y*> = ('not' x) 'or' y by Def4
.= nand2a . <*y,x*> by Def3 ; :: thesis: verum