let p be Element of CQC-WFF ; :: thesis: for x, y being bound_QC-variable 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; :: 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