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,p)*> holds
|- f ^ <*(All x,('not' ('not' p)))*>
let x be bound_QC-variable; :: thesis: for f being FinSequence of CQC-WFF st |- f ^ <*(All x,p)*> holds
|- f ^ <*(All x,('not' ('not' p)))*>
let f be FinSequence of CQC-WFF ; :: thesis: ( |- f ^ <*(All x,p)*> implies |- f ^ <*(All x,('not' ('not' p)))*> )
assume A1: |- f ^ <*(All x,p)*> ; :: thesis: |- f ^ <*(All x,('not' ('not' p)))*>
A2: ( Ant (f ^ <*(All x,p)*>) = f & Suc (f ^ <*(All x,p)*>) = All x,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 ^ <*(p . x,y0)*> by A1, A2, Th42;
then |- f ^ <*('not' ('not' (p . x,y0)))*> by Th54;
then |- f ^ <*('not' (('not' p) . x,y0))*> by Th57;
then A4: |- f ^ <*(('not' ('not' p)) . x,y0)*> by Th57;
set f1 = f ^ <*(('not' ('not' 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 A5: ( not y0 in still_not-bound_in (Ant (f ^ <*(('not' ('not' p)) . x,y0)*>)) & Suc (f ^ <*(('not' ('not' p)) . x,y0)*>) = ('not' ('not' p)) . x,y0 & not y0 in still_not-bound_in (All x,p) ) by Th5, Th60;
then not y0 in (still_not-bound_in p) \ {x} by QC_LANG3:16;
then not y0 in (still_not-bound_in ('not' p)) \ {x} by QC_LANG3:11;
then not y0 in (still_not-bound_in ('not' ('not' p))) \ {x} by QC_LANG3:11;
then not y0 in still_not-bound_in (All x,('not' ('not' p))) by QC_LANG3:16;
then |- (Ant (f ^ <*(('not' ('not' p)) . x,y0)*>)) ^ <*(All x,('not' ('not' p)))*> by A4, A5, Th43;
hence |- f ^ <*(All x,('not' ('not' p)))*> by Th5; :: thesis: verum