let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds QuantNbr (Ex (x,p)) = (QuantNbr p) + 1
let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al holds QuantNbr (Ex (x,p)) = (QuantNbr p) + 1
let x be bound_QC-variable of Al; :: 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