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