let p, q be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable holds ((All x,p) => q) => (Ex x,(p => q)) is valid
let x be bound_QC-variable; :: thesis: ((All x,p) => q) => (Ex x,(p => q)) is valid
(All x,(p '&' ('not' q))) => ((All x,p) '&' ('not' q)) is valid by Th69;
then ('not' ((All x,p) '&' ('not' q))) => ('not' (All x,(p '&' ('not' q)))) is valid by LUKASI_1:63;
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 Th26, Th34, LUKASI_1:65;
then (All x,('not' ('not' (p '&' ('not' q))))) => (All x,(p '&' ('not' q))) is valid by CQC_THE1:104;
then ('not' (All x,(p '&' ('not' q)))) => ('not' (All x,('not' ('not' (p '&' ('not' q)))))) is valid by LUKASI_1:63;
then ((All x,p) => q) => ('not' (All x,('not' ('not' (p '&' ('not' q)))))) is valid by A1, LUKASI_1:43;
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