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 q holds
(Ex (x,(p => q))) => ((All (x,p)) => 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 q holds
(Ex (x,(p => q))) => ((All (x,p)) => q) is valid
let x be bound_QC-variable of A; :: thesis: ( not x in still_not-bound_in q implies (Ex (x,(p => q))) => ((All (x,p)) => q) is valid )
assume A1: not x in still_not-bound_in q ; :: thesis: (Ex (x,(p => q))) => ((All (x,p)) => q) is valid
not x in still_not-bound_in (All (x,p)) by Th5;
then not x in still_not-bound_in ((All (x,p)) => q) by A1, Th7;
then A2: (Ex (x,((All (x,p)) => q))) => ((All (x,p)) => q) is valid by Th20;
(All (x,p)) => p is valid by CQC_THE1:66;
then A3: All (x,((p => q) => ((All (x,p)) => q))) is valid by Th23, LUKASI_1:41;
(All (x,((p => q) => ((All (x,p)) => q)))) => ((Ex (x,(p => q))) => (Ex (x,((All (x,p)) => q)))) is valid by Th34;
then (Ex (x,(p => q))) => (Ex (x,((All (x,p)) => q))) is valid by A3, CQC_THE1:65;
hence (Ex (x,(p => q))) => ((All (x,p)) => q) is valid by A2, LUKASI_1:42; :: thesis: verum