let Al be QC-alphabet ; :: thesis: 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))
let p be Element of CQC-WFF Al; :: thesis: for x, y being bound_QC-variable of Al holds ('not' p) . (x,y) = 'not' (p . (x,y))
let x, y be bound_QC-variable of Al; :: thesis: ('not' p) . (x,y) = 'not' (p . (x,y))
set S = [p,(Sbst (x,y))];
( [p,(Sbst (x,y))] `1 = p & [p,(Sbst (x,y))] `2 = Sbst (x,y) ) ;
then ( ('not' p) . (x,y) = CQC_Sub [('not' p),(Sbst (x,y))] & Sub_not [p,(Sbst (x,y))] = [('not' p),(Sbst (x,y))] ) by SUBSTUT1:def 20, SUBSTUT2:def 1;
then ('not' p) . (x,y) = 'not' (CQC_Sub [p,(Sbst (x,y))]) by SUBSTUT1:29;
hence ('not' p) . (x,y) = 'not' (p . (x,y)) by SUBSTUT2:def 1; :: thesis: verum