let Al be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al
for f being FinSequence of CQC-WFF Al 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 p, q be Element of CQC-WFF Al; :: thesis: for x, y being bound_QC-variable of Al
for f being FinSequence of CQC-WFF Al 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 of Al; :: thesis: for f being FinSequence of CQC-WFF Al 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 Al; :: 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 Th56;
A4: not y in (still_not-bound_in (f ^ <*(Ex (x,p))*>)) \/ (still_not-bound_in <*q*>) by A2, Th58;
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 Th58;
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 Th59;
then not y in (still_not-bound_in p) \ {x} by QC_LANG3:19;
then not y in (still_not-bound_in ('not' p)) \ {x} by QC_LANG3:7;
then A6: not y in still_not-bound_in (All (x,('not' p))) by QC_LANG3:12;
not y in still_not-bound_in <*q*> by A4, XBOOLE_0:def 3;
then not y in still_not-bound_in q by Th59;
then not y in still_not-bound_in ('not' q) by QC_LANG3:7;
then A7: not y in still_not-bound_in <*('not' q)*> by Th59;
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 Th58;
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