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,p))*> holds
|- f ^ <*(All (x,('not' ('not' 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,p))*> holds
|- f ^ <*(All (x,('not' ('not' p))))*>
let x be bound_QC-variable of Al; :: thesis: for f being FinSequence of CQC-WFF Al st |- f ^ <*(All (x,p))*> holds
|- f ^ <*(All (x,('not' ('not' p))))*>
let f be FinSequence of CQC-WFF Al; :: 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 of Al such that
A2: not y0 in still_not-bound_in (f ^ <*(All (x,p))*>) by Th64;
( 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 Th53;
then |- f ^ <*('not' (('not' p) . (x,y0)))*> by Th56;
then A3: |- f ^ <*(('not' ('not' p)) . (x,y0))*> by Th56;
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, 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 ^ <*(('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 Th59;
then not y0 in (still_not-bound_in p) \ {x} by QC_LANG3:12;
then not y0 in (still_not-bound_in ('not' p)) \ {x} by QC_LANG3:7;
then not y0 in (still_not-bound_in ('not' ('not' p))) \ {x} by QC_LANG3:7;
then A6: not y0 in still_not-bound_in (All (x,('not' ('not' p)))) by QC_LANG3:12;
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