let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( (Ex (x,(p => q))) => ((All (x,p)) => (Ex (x,q))) is valid & ((All (x,p)) => (Ex (x,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
( (Ex (x,(p => q))) => ((All (x,p)) => (Ex (x,q))) is valid & ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid )
let x be bound_QC-variable of A; :: thesis: ( (Ex (x,(p => q))) => ((All (x,p)) => (Ex (x,q))) is valid & ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid )
(All (x,p)) => p is valid by CQC_THE1:66;
then A1: (p => q) => ((All (x,p)) => q) is valid by LUKASI_1:41;
( not x in still_not-bound_in (All (x,p)) & not x in still_not-bound_in (Ex (x,q)) ) by Th5, Th6;
then A2: not x in still_not-bound_in ((All (x,p)) => (Ex (x,q))) by Th7;
q => (Ex (x,q)) is valid by Th15;
then (p => q) => ((All (x,p)) => (Ex (x,q))) is valid by A1, Lm16;
hence (Ex (x,(p => q))) => ((All (x,p)) => (Ex (x,q))) is valid by A2, Th19; :: thesis: ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid
(All (x,(p '&' ('not' q)))) => ((All (x,p)) '&' (All (x,('not' q)))) is valid by Th36;
then A3: ('not' ((All (x,p)) '&' (All (x,('not' q))))) => ('not' (All (x,(p '&' ('not' q))))) is valid by LUKASI_1:52;
('not' (All (x,(p '&' ('not' q))))) => (Ex (x,('not' (p '&' ('not' q))))) is valid by Th51;
then ('not' ((All (x,p)) '&' (All (x,('not' q))))) => (Ex (x,('not' (p '&' ('not' q))))) is valid by A3, LUKASI_1:42;
then A4: ('not' ((All (x,p)) '&' (All (x,('not' q))))) => (Ex (x,(p => q))) is valid by QC_LANG2:def 2;
(All (x,('not' q))) => ('not' ('not' (All (x,('not' q))))) is valid ;
then A5: ((All (x,p)) '&' (All (x,('not' q)))) => ((All (x,p)) '&' ('not' ('not' (All (x,('not' q)))))) is valid by Lm9;
(All (x,p)) => (Ex (x,q)) = (All (x,p)) => ('not' (All (x,('not' q)))) by QC_LANG2:def 5
.= 'not' ((All (x,p)) '&' ('not' ('not' (All (x,('not' q)))))) by QC_LANG2:def 2 ;
then ((All (x,p)) => (Ex (x,q))) => ('not' ((All (x,p)) '&' (All (x,('not' q))))) is valid by A5, LUKASI_1:52;
hence ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid by A4, LUKASI_1:42; :: thesis: verum