let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable holds p => (Ex x,p) is valid
let x be bound_QC-variable; :: thesis: p => (Ex x,p) is valid
(All x,('not' p)) => ('not' p) is valid by CQC_THE1:105;
then ('not' ('not' p)) => ('not' (All x,('not' p))) is valid by LUKASI_1:63;
then ( ('not' ('not' p)) => (Ex x,p) is valid & (('not' ('not' p)) => (Ex x,p)) => (p => (Ex x,p)) is valid ) by LUKASI_1:67, QC_LANG2:def 5;
hence p => (Ex x,p) is valid by CQC_THE1:104; :: thesis: verum