let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds p => (Ex (x,p)) is valid
let p be Element of CQC-WFF A; :: thesis: for x being bound_QC-variable of A holds p => (Ex (x,p)) is valid
let x be bound_QC-variable of A; :: thesis: p => (Ex (x,p)) is valid
(All (x,('not' p))) => ('not' p) is valid by CQC_THE1:66;
then ('not' ('not' p)) => ('not' (All (x,('not' p)))) is valid by LUKASI_1:52;
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:65; :: thesis: verum