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 holds
( |- f ^ <*(All (x,p))*> iff |- f ^ <*('not' (Ex (x,('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 holds
( |- f ^ <*(All (x,p))*> iff |- f ^ <*('not' (Ex (x,('not' p))))*> )
let x be bound_QC-variable of Al; :: thesis: for f being FinSequence of CQC-WFF Al holds
( |- f ^ <*(All (x,p))*> iff |- f ^ <*('not' (Ex (x,('not' p))))*> )
let f be FinSequence of CQC-WFF Al; :: thesis: ( |- f ^ <*(All (x,p))*> iff |- f ^ <*('not' (Ex (x,('not' p))))*> )
thus ( |- f ^ <*(All (x,p))*> implies |- f ^ <*('not' (Ex (x,('not' p))))*> ) :: thesis: ( |- f ^ <*('not' (Ex (x,('not' p))))*> implies |- f ^ <*(All (x,p))*> )
proof
assume |- f ^ <*(All (x,p))*> ; :: thesis: |- f ^ <*('not' (Ex (x,('not' p))))*>
then |- f ^ <*(All (x,('not' ('not' p))))*> by Th65;
then |- f ^ <*('not' ('not' (All (x,('not' ('not' p))))))*> by Th53;
hence |- f ^ <*('not' (Ex (x,('not' p))))*> by QC_LANG2:def 5; :: thesis: verum
end;
assume |- f ^ <*('not' (Ex (x,('not' p))))*> ; :: thesis: |- f ^ <*(All (x,p))*>
then |- f ^ <*('not' ('not' (All (x,('not' ('not' p))))))*> by QC_LANG2:def 5;
then |- f ^ <*(All (x,('not' ('not' p))))*> by Th54;
hence |- f ^ <*(All (x,p))*> by Th66; :: thesis: verum