Rules for usage of a colon before the label

Boris Schminke <[email protected]>
Newsgroups gmane.comp.mathematics.mizar
Message-ID <[email protected]>
Dear All,
Why some of the labels need to start with a colon, e. g.
definition
  let X be set;
  attr X is empty means
  :Def1:
  not ex x being set st x in X;
end;
After deleting the colon in this situation we will receive error messages:
::> 143: No implicit qualification
::> 321: Predicate symbol or "is" expected
On the other hand, if I add a colon before a label in more usual case
I will see messages like theese:
::> 391: Incorrect beginning of a text item
::> 396: Formula expected
It seems to me that it is a strict rule only for labels just before
the definiens, isn't it?
Yours,
Schminke Boris.
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.