[mizar] Rules for usage of a colon before the label

[Boris Schminke <schminkeba@gmail.com>]

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.