let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(Ex (x,(p => q))) => (p => (Ex (x,q))) is valid
let p, q be Element of CQC-WFF A; :: thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(Ex (x,(p => q))) => (p => (Ex (x,q))) is valid
let x be bound_QC-variable of A; :: thesis: ( not x in still_not-bound_in p implies (Ex (x,(p => q))) => (p => (Ex (x,q))) is valid )
assume A1: not x in still_not-bound_in p ; :: thesis: (Ex (x,(p => q))) => (p => (Ex (x,q))) is valid
not x in still_not-bound_in (Ex (x,q)) by Th6;
then not x in still_not-bound_in (p => (Ex (x,q))) by A1, Th7;
then A2: (Ex (x,(p => (Ex (x,q))))) => (p => (Ex (x,q))) is valid by Th20;
q => (Ex (x,q)) is valid by Th15;
then A3: All (x,((p => q) => (p => (Ex (x,q))))) is valid by Th23, LUKASI_1:51;
(All (x,((p => q) => (p => (Ex (x,q)))))) => ((Ex (x,(p => q))) => (Ex (x,(p => (Ex (x,q)))))) is valid by Th34;
then (Ex (x,(p => q))) => (Ex (x,(p => (Ex (x,q))))) is valid by A3, CQC_THE1:65;
hence (Ex (x,(p => q))) => (p => (Ex (x,q))) is valid by A2, LUKASI_1:42; :: thesis: verum