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 A1: ('not' ('not' p)) => (Ex (x,p)) is valid by QC_LANG2:def 5;
(('not' ('not' p)) => (Ex (x,p))) => (p => (Ex (x,p))) is valid ;
hence p => (Ex (x,p)) is valid by A1, CQC_THE1:104; :: thesis: verum