theorem Th50: :: BVFUNC25:96

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a '&' (b 'nand' c) = (a '&' ('not' b)) 'or' (a '&' ('not' c))