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