let x, y be Element of BOOLEAN ; :: thesis: ( or2 . <*x,y*> = nand2b . <*x,y*> & or2a . <*x,y*> = nand2a . <*y,x*> & or2b . <*x,y*> = nand2 . <*x,y*> )
thus or2 . <*x,y*> = x 'or' y by Def7
.= nand2b . <*x,y*> by Def6 ; :: thesis: ( or2a . <*x,y*> = nand2a . <*y,x*> & or2b . <*x,y*> = nand2 . <*x,y*> )
thus or2a . <*x,y*> = ('not' x) 'or' y by Def8
.= nand2a . <*y,x*> by Def5 ; :: thesis: or2b . <*x,y*> = nand2 . <*x,y*>
thus or2b . <*x,y*> = ('not' x) 'or' ('not' y) by Def9
.= nand2 . <*x,y*> by Def4 ; :: thesis: verum