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.