let A be QC-alphabet ; for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,p)) => (Ex (x,p)) is valid
let p be Element of CQC-WFF A; for x being bound_QC-variable of A holds (All (x,p)) => (Ex (x,p)) is valid
let x be bound_QC-variable of A; (All (x,p)) => (Ex (x,p)) is valid
( (All (x,p)) => p is valid & p => (Ex (x,p)) is valid )
by Th15, CQC_THE1:66;
hence
(All (x,p)) => (Ex (x,p)) is valid
by LUKASI_1:42; verum