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 that
A1: p = h . x and
A2: q = h . y and
A3: not y in still_not-bound_in h ; :: thesis: p => (Ex y,q) is valid
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) by Th6;
then A5: not y in still_not-bound_in (h => (Ex y,q)) by A3, Th7;
A6: q => (Ex y,q) is valid by Th18;
(h => (Ex y,q)) . y = (h . y) => ((Ex y,q) . y) by Th14
.= q => (Ex y,q) by A2, CQC_LANG:40 ;
hence p => (Ex y,q) is valid by A6, A4, A5, CQC_THE1:107; :: thesis: verum