theorem Th56: :: CALCUL_1:57

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al holds ('not' p) . (x,y) = 'not' (p . (x,y))