real number vs. Element of REAL

There is known problem: which one to use? The denotation is the same, 
however technically the type 'real number' is more general than 
'Element of REAL'
Therefore one likes to have theorems about real numbers and one likes 
to prove theorems about elements of reals. The same goes for other 
kinds of numbers.
However short notation (expandable type) is used as a rule for 'number' 
with an adjective:

ORDINAL1:
   mode Nat is natural number;
INT_1:
   mode Integer is integer number;
RAT_1:
   mode Rational is rational number;
CFUNCT_1:
   mode Complex is complex number;

not so in the case of 'Real':

REAL_1:
   mode Real is Element of REAL;

If there are some arguments for both types, it is unacceptable that the 
user must look to the abstracts to check which type had been used in 
the theorem to which he wants to refer to. And if we have to choose, 
'real number' is preferable.

Changing the definition of the mode 'Real' causes too many errors, co 
some preparatory work is necessary. In the new version many occurrences 
of
'Real' are changed to 'real number'. With more than 600 articles 
modified we decided to publish this new version of MML, even if the 
revolution is not completed. Sorry for the (even bigger) mess, we will 
correct it ASAP.

Regards,
Andrzej