let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds
p => (Ex (y,q)) is valid
let p, q be Element of CQC-WFF A; :: thesis: for h being QC-formula of A
for x, y being bound_QC-variable of A 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 of A; :: thesis: for x, y being bound_QC-variable of A 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 of A; :: 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 Th12
.= p => (Ex (y,q)) by A1, CQC_LANG:27 ;
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 Th15;
(h => (Ex (y,q))) . y = (h . y) => ((Ex (y,q)) . y) by Th12
.= q => (Ex (y,q)) by A2, CQC_LANG:27 ;
hence p => (Ex (y,q)) is valid by A6, A4, A5, CQC_THE1:68; :: thesis: verum