let Al be 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)) & ( QuantNbr p = QuantNbr (p . (x,y)) implies QuantNbr ('not' p) = QuantNbr ('not' (p . (x,y))) ) )
let p be Element of CQC-WFF Al; for x, y being bound_QC-variable of Al holds
( 'not' (p . (x,y)) = 'not' (p . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) implies QuantNbr ('not' p) = QuantNbr ('not' (p . (x,y))) ) )
let x, y be bound_QC-variable of Al; ( 'not' (p . (x,y)) = 'not' (p . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) implies QuantNbr ('not' p) = QuantNbr ('not' (p . (x,y))) ) )
set S = [('not' p),(Sbst (x,y))];
A1:
[('not' p),(Sbst (x,y))] = Sub_not [p,(Sbst (x,y))]
by Th16;
then A2:
('not' p) . (x,y) = 'not' (CQC_Sub [p,(Sbst (x,y))])
by SUBSTUT1:29;
( QuantNbr p = QuantNbr (p . (x,y)) implies QuantNbr ('not' p) = QuantNbr (('not' p) . (x,y)) )
hence
( 'not' (p . (x,y)) = 'not' (p . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) implies QuantNbr ('not' p) = QuantNbr ('not' (p . (x,y))) ) )
by A1, SUBSTUT1:29; verum