let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable
for f being FinSequence of CQC-WFF st |- f ^ <*(All x,('not' ('not' p)))*> holds
|- f ^ <*(All x,p)*>
let x be bound_QC-variable; :: thesis: for f being FinSequence of CQC-WFF st |- f ^ <*(All x,('not' ('not' p)))*> holds
|- f ^ <*(All x,p)*>
let f be FinSequence of CQC-WFF ; :: 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 such that
A2: not y0 in still_not-bound_in (f ^ <*(All x,p)*>) by Th65;
( 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 Th57;
then A3: |- f ^ <*('not' ('not' (p . x,y0)))*> by Th57;
set f1 = f ^ <*(p . x,y0)*>;
A4: not y0 in (still_not-bound_in f) \/ (still_not-bound_in <*(All x,p)*>) by A2, Th59;
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 Th60;
Suc (f ^ <*(p . x,y0)*>) = p . x,y0 by Th5;
then |- (Ant (f ^ <*(p . x,y0)*>)) ^ <*(All x,p)*> by A3, A5, A6, Th43, Th55;
hence |- f ^ <*(All x,p)*> by Th5; :: thesis: verum