let x, y, z be Element of BOOLEAN ; :: thesis: ( and3 . <*x,y,z*> = nor3c . <*x,y,z*> & and3a . <*x,y,z*> = nor3b . <*z,y,x*> & and3b . <*x,y,z*> = nor3a . <*z,y,x*> & and3c . <*x,y,z*> = nor3 . <*x,y,z*> )
thus and3 . <*x,y,z*> = 'not' (('not' ('not' (('not' x) 'or' ('not' y)))) 'or' ('not' z)) by Def16
.= nor3c . <*x,y,z*> by Def31 ; :: thesis: ( and3a . <*x,y,z*> = nor3b . <*z,y,x*> & and3b . <*x,y,z*> = nor3a . <*z,y,x*> & and3c . <*x,y,z*> = nor3 . <*x,y,z*> )
thus and3a . <*x,y,z*> = 'not' (('not' ('not' (('not' ('not' x)) 'or' ('not' y)))) 'or' ('not' z)) by Def17
.= 'not' ((('not' z) 'or' ('not' y)) 'or' x)
.= nor3b . <*z,y,x*> by Def30 ; :: thesis: ( and3b . <*x,y,z*> = nor3a . <*z,y,x*> & and3c . <*x,y,z*> = nor3 . <*x,y,z*> )
thus and3b . <*x,y,z*> = 'not' (('not' ('not' (('not' ('not' x)) 'or' ('not' ('not' y))))) 'or' ('not' z)) by Def18
.= 'not' ((('not' z) 'or' y) 'or' x)
.= nor3a . <*z,y,x*> by Def29 ; :: thesis: and3c . <*x,y,z*> = nor3 . <*x,y,z*>
thus and3c . <*x,y,z*> = 'not' (('not' ('not' (('not' ('not' x)) 'or' ('not' ('not' y))))) 'or' ('not' ('not' z))) by Def19
.= nor3 . <*x,y,z*> by Def28 ; :: thesis: verum