theorem :: XBOOLEAN:51

for p being boolean object holds p 'nand' p = 'not' p ;