let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable
for f being FinSequence of CQC-WFF holds
( |- f ^ <*(All (x,p))*> iff |- f ^ <*('not' (Ex (x,('not' p))))*> )
let x be bound_QC-variable; :: thesis: for f being FinSequence of CQC-WFF holds
( |- f ^ <*(All (x,p))*> iff |- f ^ <*('not' (Ex (x,('not' p))))*> )
let f be FinSequence of CQC-WFF ; :: 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 Th66;
then |- f ^ <*('not' ('not' (All (x,('not' ('not' p))))))*> by Th54;
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 Th55;
hence |- f ^ <*(All (x,p))*> by Th67; :: thesis: verum