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