I have solved it now. But not by myself. I used a proof on this page: https://math.stackexchange.com/questions/140197/what-is-a-constructive-proof-of-lnot-lnotp-vee-lnot-p :
In Fitch style: [image: Proof in Fitch style] <https://i.stack.imgur.com/jfmEy.png> > > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/44422114-647b-490d-a3d3-ab29b7776ede%40googlegroups.com.
