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)))*>
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,p)*>) = f & Suc (f ^ <*(All x,p)*>) = All x,p ) by Th5;
then |- f ^ <*(p . x,y0)*> by A1, Th42;
then |- f ^ <*('not' ('not' (p . x,y0)))*> by Th54;
then |- f ^ <*('not' (('not' p) . x,y0))*> by Th57;
then A3: |- f ^ <*(('not' ('not' p)) . x,y0)*> by Th57;
set f1 = f ^ <*(('not' ('not' 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 ^ <*(('not' ('not' p)) . x,y0)*>)) by Th5;
not y0 in still_not-bound_in <*(All x,p)*> by A4, XBOOLE_0:def 3;
then not y0 in still_not-bound_in (All x,p) by 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 A6: not y0 in still_not-bound_in (All x,('not' ('not' p))) by QC_LANG3:16;
Suc (f ^ <*(('not' ('not' p)) . x,y0)*>) = ('not' ('not' p)) . x,y0 by Th5;
then |- (Ant (f ^ <*(('not' ('not' p)) . x,y0)*>)) ^ <*(All x,('not' ('not' p)))*> by A3, A5, A6, Th43;
hence |- f ^ <*(All x,('not' ('not' p)))*> by Th5; :: thesis: verum