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)*>
A2: ( Ant (f ^ <*(All x,('not' ('not' p)))*>) = f & Suc (f ^ <*(All x,('not' ('not' p)))*>) = All x,('not' ('not' p)) ) by Th5;
consider y0 being bound_QC-variable such that
A3: not y0 in still_not-bound_in (f ^ <*(All x,p)*>) by Th65;
|- f ^ <*(('not' ('not' p)) . x,y0)*> by A1, A2, Th42;
then |- f ^ <*('not' (('not' p) . x,y0))*> by Th57;
then A4: |- f ^ <*('not' ('not' (p . x,y0)))*> by Th57;
set f1 = f ^ <*(p . x,y0)*>;
not y0 in (still_not-bound_in f) \/ (still_not-bound_in <*(All x,p)*>) by A3, Th59;
then ( not y0 in still_not-bound_in f & not y0 in still_not-bound_in <*(All x,p)*> ) by XBOOLE_0:def 3;
then ( not y0 in still_not-bound_in (Ant (f ^ <*(p . x,y0)*>)) & Suc (f ^ <*(p . x,y0)*>) = p . x,y0 & not y0 in still_not-bound_in (All x,p) ) by Th5, Th60;
then |- (Ant (f ^ <*(p . x,y0)*>)) ^ <*(All x,p)*> by A4, Th43, Th55;
hence |- f ^ <*(All x,p)*> by Th5; :: thesis: verum