4.8.3 Warning About Labels

Further, we will give a warning about labels. In Mizar, it is acceptable to use the same label; however, the ones just before are prioritized.

For example:


       L1:......;
          ......
       L1:......;
          ...... by L1; Here, L1 of just before is cited.


    When we want to demonstrate something with this case, if we state by L1, the sentence of L1 below it will be cited.
    This is easily mistaken and when we put labels L1,L2,L3,...... , we tend to forget until the labels were used. Also, let us assume that we put L3 and when we state by L3, even if we think that it is L3 and we can certainly infer from L3, there will be an error. This kind of mistake is made often at first. When this happens, there is one same label that is hiding if examined carefully. Sometimes, there is another one in a different place.