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)) & ( QuantNbr p = QuantNbr (p . (x,y)) implies QuantNbr ('not' p) = QuantNbr ('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)) & ( QuantNbr p = QuantNbr (p . (x,y)) implies QuantNbr ('not' p) = QuantNbr ('not' (p . (x,y))) ) )
let x, y be bound_QC-variable of Al; :: thesis: ( '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)) )

proof

assume A3: QuantNbr p = QuantNbr (p . (x,y)) ; :: thesis: QuantNbr ('not' p) = QuantNbr (('not' p) . (x,y))
QuantNbr (('not' p) . (x,y)) = QuantNbr (p . (x,y)) by A2, CQC_SIM1:16;
hence QuantNbr ('not' p) = QuantNbr (('not' p) . (x,y)) by A3, CQC_SIM1:16; :: thesis: verum

end;

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; :: thesis: verum