let p, q be Element of CQC-WFF ; :: thesis: for x, y being bound_QC-variable
for f being FinSequence of CQC-WFF st |- (f ^ <*(p . x,y)*>) ^ <*q*> & not y in still_not-bound_in ((f ^ <*(Ex x,p)*>) ^ <*q*>) holds
|- (f ^ <*(Ex x,p)*>) ^ <*q*>
let x, y be bound_QC-variable; :: thesis: for f being FinSequence of CQC-WFF st |- (f ^ <*(p . x,y)*>) ^ <*q*> & not y in still_not-bound_in ((f ^ <*(Ex x,p)*>) ^ <*q*>) holds
|- (f ^ <*(Ex x,p)*>) ^ <*q*>
let f be FinSequence of CQC-WFF ; :: thesis: ( |- (f ^ <*(p . x,y)*>) ^ <*q*> & not y in still_not-bound_in ((f ^ <*(Ex x,p)*>) ^ <*q*>) implies |- (f ^ <*(Ex x,p)*>) ^ <*q*> )
assume A1: ( |- (f ^ <*(p . x,y)*>) ^ <*q*> & not y in still_not-bound_in ((f ^ <*(Ex x,p)*>) ^ <*q*>) ) ; :: thesis: |- (f ^ <*(Ex x,p)*>) ^ <*q*>
then |- (f ^ <*('not' q)*>) ^ <*('not' (p . x,y))*> by Th46;
then A2: |- (f ^ <*('not' q)*>) ^ <*(('not' p) . x,y)*> by Th57;
set f1 = (f ^ <*('not' q)*>) ^ <*(('not' p) . x,y)*>;
not y in (still_not-bound_in (f ^ <*(Ex x,p)*>)) \/ (still_not-bound_in <*q*>) by A1, Th59;
then A3: ( not y in still_not-bound_in (f ^ <*(Ex x,p)*>) & not y in still_not-bound_in <*q*> ) by XBOOLE_0:def 3;
then not y in still_not-bound_in q by Th60;
then A4: ( not y in (still_not-bound_in f) \/ (still_not-bound_in <*(Ex x,p)*>) & not y in still_not-bound_in ('not' q) ) by A3, Th59, QC_LANG3:11;
then A5: ( not y in still_not-bound_in f & not y in still_not-bound_in <*(Ex x,p)*> ) by XBOOLE_0:def 3;
not y in still_not-bound_in <*('not' q)*> by A4, Th60;
then not y in (still_not-bound_in f) \/ (still_not-bound_in <*('not' q)*>) by A5, XBOOLE_0:def 3;
then not y in still_not-bound_in (f ^ <*('not' q)*>) by Th59;
then A6: ( not y in still_not-bound_in (Ant ((f ^ <*('not' q)*>) ^ <*(('not' p) . x,y)*>)) & Suc ((f ^ <*('not' q)*>) ^ <*(('not' p) . x,y)*>) = ('not' p) . x,y ) by Th5;
not y in still_not-bound_in (Ex x,p) by A5, Th60;
then not y in (still_not-bound_in p) \ {x} by QC_LANG3:23;
then not y in (still_not-bound_in ('not' p)) \ {x} by QC_LANG3:11;
then not y in still_not-bound_in (All x,('not' p)) by QC_LANG3:16;
then |- (Ant ((f ^ <*('not' q)*>) ^ <*(('not' p) . x,y)*>)) ^ <*(All x,('not' p))*> by A2, A6, Th43;
then |- (f ^ <*('not' q)*>) ^ <*(All x,('not' p))*> by Th5;
then |- (f ^ <*('not' (All x,('not' p)))*>) ^ <*q*> by Th48;
hence |- (f ^ <*(Ex x,p)*>) ^ <*q*> by QC_LANG2:def 5; :: thesis: verum