let p, q be Element of CQC-WFF ; :: thesis: for h being QC-formula
for x, y being bound_QC-variable st p = h . x & q = h . y & not y in still_not-bound_in h holds
p => (Ex y,q) is valid
let h be QC-formula; :: thesis: for x, y being bound_QC-variable st p = h . x & q = h . y & not y in still_not-bound_in h holds
p => (Ex y,q) is valid
let x, y be bound_QC-variable; :: thesis: ( p = h . x & q = h . y & not y in still_not-bound_in h implies p => (Ex y,q) is valid )
assume A1: ( p = h . x & q = h . y & not y in still_not-bound_in h ) ; :: thesis: p => (Ex y,q) is valid
A2: q => (Ex y,q) is valid by Th18;
A3: (h => (Ex y,q)) . y = (h . y) => ((Ex y,q) . y) by Th14
.= q => (Ex y,q) by A1, CQC_LANG:40 ;
A4: (h => (Ex y,q)) . x = (h . x) => ((Ex y,q) . x) by Th14
.= p => (Ex y,q) by A1, CQC_LANG:40 ;
( not y in still_not-bound_in (Ex y,q) & not y in still_not-bound_in h ) by A1, Th6;
then not y in still_not-bound_in (h => (Ex y,q)) by Th7;
hence p => (Ex y,q) is valid by A2, A3, A4, CQC_THE1:107; :: thesis: verum