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 |- f ^ <*(All (x,('not' ('not' p))))*> holds
|- f ^ <*(All (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 |- f ^ <*(All (x,('not' ('not' p))))*> holds
|- f ^ <*(All (x,p))*>
let x be bound_QC-variable of Al; :: thesis: for f being FinSequence of CQC-WFF Al st |- f ^ <*(All (x,('not' ('not' p))))*> holds
|- f ^ <*(All (x,p))*>
let f be FinSequence of CQC-WFF Al; :: thesis: ( |- f ^ <*(All (x,('not' ('not' p))))*> implies |- f ^ <*(All (x,p))*> )
assume A1: |- f ^ <*(All (x,('not' ('not' p))))*> ; :: thesis: |- f ^ <*(All (x,p))*>
consider y0 being bound_QC-variable of Al such that
A2: not y0 in still_not-bound_in (f ^ <*(All (x,p))*>) by Th64;
( Ant (f ^ <*(All (x,('not' ('not' p))))*>) = f & Suc (f ^ <*(All (x,('not' ('not' p))))*>) = All (x,('not' ('not' p))) ) by Th5;
then |- f ^ <*(('not' ('not' p)) . (x,y0))*> by A1, Th42;
then |- f ^ <*('not' (('not' p) . (x,y0)))*> by Th56;
then A3: |- f ^ <*('not' ('not' (p . (x,y0))))*> by Th56;
set f1 = f ^ <*(p . (x,y0))*>;
A4: not y0 in (still_not-bound_in f) \/ (still_not-bound_in <*(All (x,p))*>) by A2, Th58;
then not y0 in still_not-bound_in f by XBOOLE_0:def 3;
then A5: not y0 in still_not-bound_in (Ant (f ^ <*(p . (x,y0))*>)) by Th5;
not y0 in still_not-bound_in <*(All (x,p))*> by A4, XBOOLE_0:def 3;
then A6: not y0 in still_not-bound_in (All (x,p)) by Th59;
Suc (f ^ <*(p . (x,y0))*>) = p . (x,y0) by Th5;
then |- (Ant (f ^ <*(p . (x,y0))*>)) ^ <*(All (x,p))*> by A3, A5, A6, Th43, Th54;
hence |- f ^ <*(All (x,p))*> by Th5; :: thesis: verum