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