let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable holds QuantNbr (Ex x,p) = (QuantNbr p) + 1
let x be bound_QC-variable; :: thesis: QuantNbr (Ex x,p) = (QuantNbr p) + 1
QuantNbr (Ex x,p) = QuantNbr ('not' (All x,('not' p))) by QC_LANG2:def 5
.= QuantNbr (All x,('not' p)) by CQC_SIM1:16
.= (QuantNbr ('not' p)) + 1 by CQC_SIM1:18 ;
hence QuantNbr (Ex x,p) = (QuantNbr p) + 1 by CQC_SIM1:16; :: thesis: verum