let p, q be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable holds (p => (Ex x,q)) => (Ex x,(p => q)) is valid
let x be bound_QC-variable; :: thesis: (p => (Ex x,q)) => (Ex x,(p => q)) is valid
( 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;
then (All x,('not' ('not' (p '&' ('not' q))))) => (All x,(p '&' ('not' q))) is valid by CQC_THE1:104;
then A1: ('not' (All x,(p '&' ('not' q)))) => ('not' (All x,('not' ('not' (p '&' ('not' q)))))) is valid by LUKASI_1:63;
(All x,('not' q)) <=> ('not' (Ex x,q)) is valid by Th58;
then (All x,('not' q)) => ('not' (Ex x,q)) is valid by Lm14;
then (p '&' (All x,('not' q))) => (p '&' ('not' (Ex x,q))) is valid by Lm9;
then A2: ('not' (p '&' ('not' (Ex x,q)))) => ('not' (p '&' (All x,('not' q)))) is valid by LUKASI_1:63;
(All x,(p '&' ('not' q))) => (p '&' (All x,('not' q))) is valid by Th68;
then ('not' (p '&' (All x,('not' q)))) => ('not' (All x,(p '&' ('not' q)))) is valid by LUKASI_1:63;
then ('not' (p '&' ('not' (Ex x,q)))) => ('not' (All x,(p '&' ('not' q)))) is valid by A2, LUKASI_1:43;
then (p => (Ex x,q)) => ('not' (All x,(p '&' ('not' q)))) is valid by QC_LANG2:def 2;
then (p => (Ex x,q)) => ('not' (All x,('not' ('not' (p '&' ('not' q)))))) is valid by A1, LUKASI_1:43;
then (p => (Ex x,q)) => ('not' (All x,('not' (p => q)))) is valid by QC_LANG2:def 2;
hence (p => (Ex x,q)) => (Ex x,(p => q)) is valid by QC_LANG2:def 5; :: thesis: verum