4.8.3　ラベルについての注意

　それから，ここでラベルの注意をしておきます．Mizar では，同じラベルを使ってもかまいませんが，直前のものが優先されます．
　例えば，

　　　　　L1:......;
　　　　　　　 ......
　　　　　L1:......;
　　　　　　　 ...... by L1; ここでは直前の L1 が引用される


　この例で何か証明したときに by L1 とすると，下の L1 の文が引用されます．
　このことは間違いやすく L1, L2, L3, . . . . . . とラベルをつけていって，どこまでラベルを使ったのかを忘れてしまい，また L3 とつけたとします．そして，by L3 とすると，自分では前の L3 のつもりで必ず L3 から推論できると思っても，いくらやってもエラーがでてきてしまうわけです．このようなことを最初のうちによくやります．このときはよく捜すと，同じラベルが1つ隠れているのです．もうひとつ別のところにあることがあります．