let x, y, z be Element of BOOLEAN ; :: thesis: ( or3 . <*x,y,z*> = nand3c . <*x,y,z*> & or3a . <*x,y,z*> = nand3b . <*z,y,x*> & or3b . <*x,y,z*> = nand3a . <*z,y,x*> & or3c . <*x,y,z*> = nand3 . <*x,y,z*> )
thus or3 . <*x,y,z*> = (x 'or' y) 'or' z by Def24
.= nand3c . <*x,y,z*> by Def23 ; :: thesis: ( or3a . <*x,y,z*> = nand3b . <*z,y,x*> & or3b . <*x,y,z*> = nand3a . <*z,y,x*> & or3c . <*x,y,z*> = nand3 . <*x,y,z*> )
thus or3a . <*x,y,z*> = (('not' x) 'or' y) 'or' z by Def25
.= 'not' ((('not' z) '&' ('not' y)) '&' x)
.= nand3b . <*z,y,x*> by Def22 ; :: thesis: ( or3b . <*x,y,z*> = nand3a . <*z,y,x*> & or3c . <*x,y,z*> = nand3 . <*x,y,z*> )
thus or3b . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' z by Def26
.= 'not' ((('not' z) '&' y) '&' x)
.= nand3a . <*z,y,x*> by Def21 ; :: thesis: or3c . <*x,y,z*> = nand3 . <*x,y,z*>
thus or3c . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' ('not' z) by Def27
.= nand3 . <*x,y,z*> by Def20 ; :: thesis: verum