Jan Burse schrieb: > It can be used in connection with some double negation > translation (DNT) to show the corrolar that an intuitionistic > consequence is also a classical consequence. P.S.: I don't mean Glivenko's theorem itself by the above.