theorem :: XBOOLEAN:54

for p, q, r being boolean object holds p 'nand' (q 'nand' r) = (('not' p) 'or' q) '&' (('not' p) 'or' r)