let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds ((All (x,p)) => q) => (Ex (x,(p => q))) is valid
let p, q be Element of CQC-WFF A; :: thesis: for x being bound_QC-variable of A holds ((All (x,p)) => q) => (Ex (x,(p => q))) is valid
let x be bound_QC-variable of A; :: thesis: ((All (x,p)) => q) => (Ex (x,(p => q))) is valid
(All (x,(p '&' ('not' q)))) => ((All (x,p)) '&' ('not' q)) is valid by Th65;
then ('not' ((All (x,p)) '&' ('not' q))) => ('not' (All (x,(p '&' ('not' q))))) is valid by LUKASI_1:52;
then A1: ((All (x,p)) => q) => ('not' (All (x,(p '&' ('not' q))))) is valid by QC_LANG2:def 2;
( All (x,(('not' ('not' (p '&' ('not' q)))) => (p '&' ('not' q)))) is valid & (All (x,(('not' ('not' (p '&' ('not' q)))) => (p '&' ('not' q))))) => ((All (x,('not' ('not' (p '&' ('not' q)))))) => (All (x,(p '&' ('not' q))))) is valid ) by Th23, Th30;
then (All (x,('not' ('not' (p '&' ('not' q)))))) => (All (x,(p '&' ('not' q)))) is valid by CQC_THE1:65;
then ('not' (All (x,(p '&' ('not' q))))) => ('not' (All (x,('not' ('not' (p '&' ('not' q))))))) is valid by LUKASI_1:52;
then ((All (x,p)) => q) => ('not' (All (x,('not' ('not' (p '&' ('not' q))))))) is valid by A1, LUKASI_1:42;
then ((All (x,p)) => q) => (Ex (x,('not' (p '&' ('not' q))))) is valid by QC_LANG2:def 5;
hence ((All (x,p)) => q) => (Ex (x,(p => q))) is valid by QC_LANG2:def 2; :: thesis: verum