let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for r being Element of CQC-WFF A holds Ex (x,r) is Element of CQC-WFF A
let x be bound_QC-variable of A; :: thesis: for r being Element of CQC-WFF A holds Ex (x,r) is Element of CQC-WFF A
let r be Element of CQC-WFF A; :: thesis: Ex (x,r) is Element of CQC-WFF A
Ex (x,r) = 'not' (All (x,('not' r))) by QC_LANG2:def 5;
hence Ex (x,r) is Element of CQC-WFF A ; :: thesis: verum