let x, y, z be Element of BOOLEAN ; :: thesis: ( and3a . <*x,y,z*> = nor3b . <*z,y,x*> & and3b . <*x,y,z*> = nor3a . <*z,y,x*> )
thus and3a . <*x,y,z*> = 'not' (('not' ('not' (('not' ('not' x)) 'or' ('not' y)))) 'or' ('not' z)) by Def10
.= 'not' ((('not' z) 'or' ('not' y)) 'or' x)
.= nor3b . <*z,y,x*> by Def19 ; :: thesis: and3b . <*x,y,z*> = nor3a . <*z,y,x*>
thus and3b . <*x,y,z*> = 'not' (('not' ('not' (('not' ('not' x)) 'or' ('not' ('not' y))))) 'or' ('not' z)) by Def11
.= 'not' ((('not' z) 'or' y) 'or' x)
.= nor3a . <*z,y,x*> by Def18 ; :: thesis: verum