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
(All x,p) => p is valid by CQC_THE1:105;
then (p => q) => ((All x,p) => q) is valid by LUKASI_1:42;
then ( All x,((p => q) => ((All x,p) => q)) is valid & (All x,((p => q) => ((All x,p) => q))) => ((Ex x,(p => q)) => (Ex x,((All x,p) => q))) is valid ) by Th26, Th38;
then A2: (Ex x,(p => q)) => (Ex x,((All x,p) => q)) is valid by CQC_THE1:104;
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 (Ex x,((All x,p) => q)) => ((All x,p) => q) is valid by Th23;
hence (Ex x,(p => q)) => ((All x,p) => q) is valid by A2, LUKASI_1:43; :: thesis: verum