4.5.1 Caution About End
As a caution about end, in Mizar, end is used in many ways such as proof
∼ end and now ∼ end. These have been nesting. When there are many ends,
we get confused on which end is which. Therefore, because end is needed
when now is written, we should write end as soon as writing now. The rest
is just filling this in with an editor. In the same way, we should write
end as soon as a proof is written. We will not make any mistakes if we
just remember that end will not be written automatically.