let p be Element of CQC-WFF ; :: thesis: for x, y being bound_QC-variable holds (All x,p) => (Ex y,p) is valid
let x, y be bound_QC-variable; :: thesis: (All x,p) => (Ex y,p) is valid
( (All x,p) => p is valid & p => (Ex y,p) is valid ) by Th18, CQC_THE1:105;
hence (All x,p) => (Ex y,p) is valid by LUKASI_1:43; :: thesis: verum