let x, y, z be Element of BOOLEAN ; :: thesis: ( or3a . <*x,y,z*> = nand3b . <*z,y,x*> & or3b . <*x,y,z*> = nand3a . <*z,y,x*> )
thus or3a . <*x,y,z*> = (('not' x) 'or' y) 'or' z by Def15
.= 'not' ((('not' z) '&' ('not' y)) '&' x)
.= nand3b . <*z,y,x*> by Def14 ; :: thesis: or3b . <*x,y,z*> = nand3a . <*z,y,x*>
thus or3b . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' z by Def16
.= 'not' ((('not' z) '&' y) '&' x)
.= nand3a . <*z,y,x*> by Def13 ; :: thesis: verum