let q, p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable 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; :: 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 Th23;
(All (x,p)) => p is valid by CQC_THE1:66;
then A3: All (x,((p => q) => ((All (x,p)) => q))) is valid by Th26, LUKASI_1:41;
(All (x,((p => q) => ((All (x,p)) => q)))) => ((Ex (x,(p => q))) => (Ex (x,((All (x,p)) => q)))) is valid by Th38;
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