let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for f being FinSequence of CQC-WFF Al st ex y being bound_QC-variable of Al st |- f ^ <*(p . (x,y))*> holds
|- f ^ <*(Ex (x,p))*>
let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al
for f being FinSequence of CQC-WFF Al st ex y being bound_QC-variable of Al st |- f ^ <*(p . (x,y))*> holds
|- f ^ <*(Ex (x,p))*>
let x be bound_QC-variable of Al; :: thesis: for f being FinSequence of CQC-WFF Al st ex y being bound_QC-variable of Al st |- f ^ <*(p . (x,y))*> holds
|- f ^ <*(Ex (x,p))*>
let f be FinSequence of CQC-WFF Al; :: thesis: ( ex y being bound_QC-variable of Al st |- f ^ <*(p . (x,y))*> implies |- f ^ <*(Ex (x,p))*> )
given y being bound_QC-variable of Al such that A1: |- f ^ <*(p . (x,y))*> ; :: thesis: |- f ^ <*(Ex (x,p))*>
set f1 = (f ^ <*(All (x,('not' p)))*>) ^ <*(All (x,('not' p)))*>;
A2: Ant ((f ^ <*(All (x,('not' p)))*>) ^ <*(All (x,('not' p)))*>) = f ^ <*(All (x,('not' p)))*> by Th5;
(len f) + 1 = (len f) + (len <*(All (x,('not' p)))*>) by FINSEQ_1:39;
then (len f) + 1 = len (Ant ((f ^ <*(All (x,('not' p)))*>) ^ <*(All (x,('not' p)))*>)) by A2, FINSEQ_1:22;
then A3: (len f) + 1 in dom (Ant ((f ^ <*(All (x,('not' p)))*>) ^ <*(All (x,('not' p)))*>)) by A2, Th10;
A4: Suc ((f ^ <*(All (x,('not' p)))*>) ^ <*(All (x,('not' p)))*>) = All (x,('not' p)) by Th5;
(Ant ((f ^ <*(All (x,('not' p)))*>) ^ <*(All (x,('not' p)))*>)) . ((len f) + 1) = All (x,('not' p)) by A2, FINSEQ_1:42;
then Suc ((f ^ <*(All (x,('not' p)))*>) ^ <*(All (x,('not' p)))*>) is_tail_of Ant ((f ^ <*(All (x,('not' p)))*>) ^ <*(All (x,('not' p)))*>) by A4, A3, Lm2;
then |- (f ^ <*(All (x,('not' p)))*>) ^ <*(('not' p) . (x,y))*> by A2, A4, Th33, Th42;
then |- (f ^ <*(All (x,('not' p)))*>) ^ <*('not' (p . (x,y)))*> by Th56;
then |- (f ^ <*(p . (x,y))*>) ^ <*('not' (All (x,('not' p))))*> by Th49;
then A5: |- (f ^ <*(p . (x,y))*>) ^ <*(Ex (x,p))*> by QC_LANG2:def 5;
1 <= len (f ^ <*(p . (x,y))*>) by Th10;
then |- (Ant (f ^ <*(p . (x,y))*>)) ^ <*(Ex (x,p))*> by A1, A5, Th45;
hence |- f ^ <*(Ex (x,p))*> by Th5; :: thesis: verum