This is to track the problem with [set.mm#3452](https://github.com/metamath/set.mm/pull/3452). At first sight, it looks like the labels in the comment section are wrongfully considered as part of a proof.