Zero or empty set

[Andrzej Trybulec <trybulec@wwwserve.cs.shinshu-u.ac.jp>]

A numeral is defined (in Mizar) as
 either 
  a. a string of digits starting with a non zero digit
 or
  b. the string "0".

I think that maybe we should rather introduce "0" as a functor symbol
and simplify the definition of a numeral;
The 0 equals the empty set (the von Neuman construction of natural
numbers
is used in Mizar) and if it was a functor symbol, it could be used as
the symbol of the empty set (and d237 eliminated).

Then a functor registration of clusters would be for 0 allowed. It is
important because 0, actually empty set, has a lot of properties
(represented by adjective, of course) that better be used automatically.
E.g. it is a function, a relation, a function-yielding function and so
on.

Comments are appreciated.

Andrzej Trybulec