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