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 that
A1: |- (f ^ <*(p . x,y)*>) ^ <*q*> and
A2: not y in still_not-bound_in ((f ^ <*(Ex x,p)*>) ^ <*q*>) ; :: thesis: |- (f ^ <*(Ex x,p)*>) ^ <*q*>
set f1 = (f ^ <*('not' q)*>) ^ <*(('not' p) . x,y)*>;
|- (f ^ <*('not' q)*>) ^ <*('not' (p . x,y))*> by A1, Th46;
then A3: |- (f ^ <*('not' q)*>) ^ <*(('not' p) . x,y)*> by Th57;
A4: not y in (still_not-bound_in (f ^ <*(Ex x,p)*>)) \/ (still_not-bound_in <*q*>) by A2, Th59;
then not y in still_not-bound_in (f ^ <*(Ex x,p)*>) by XBOOLE_0:def 3;
then A5: not y in (still_not-bound_in f) \/ (still_not-bound_in <*(Ex x,p)*>) by Th59;
then not y in still_not-bound_in <*(Ex x,p)*> by XBOOLE_0:def 3;
then not y in still_not-bound_in (Ex x,p) by 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 A6: not y in still_not-bound_in (All x,('not' p)) by QC_LANG3:16;
not y in still_not-bound_in <*q*> by A4, XBOOLE_0:def 3;
then not y in still_not-bound_in q by Th60;
then not y in still_not-bound_in ('not' q) by QC_LANG3:11;
then A7: not y in still_not-bound_in <*('not' q)*> by Th60;
not y in still_not-bound_in f by A5, XBOOLE_0:def 3;
then not y in (still_not-bound_in f) \/ (still_not-bound_in <*('not' q)*>) by A7, XBOOLE_0:def 3;
then not y in still_not-bound_in (f ^ <*('not' q)*>) by Th59;
then A8: not y in still_not-bound_in (Ant ((f ^ <*('not' q)*>) ^ <*(('not' p) . x,y)*>)) by Th5;
Suc ((f ^ <*('not' q)*>) ^ <*(('not' p) . x,y)*>) = ('not' p) . x,y by Th5;
then |- (Ant ((f ^ <*('not' q)*>) ^ <*(('not' p) . x,y)*>)) ^ <*(All x,('not' p))*> by A3, A8, 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