Ordered Rings

[Christoph Schwarzweller <schwarzw@informatik.uni-tuebingen.de>]

Hi,

We are thinking about introducing ordered rings in Mizar.
The question is how to introduce the order:

  - extending the structure by an additional field and defining 
    necessary attributes (reflexivity, ... or whatever) about 
    this field 

or

  - by an internal definition without an additional field in 
    the structure, that is defining the set of positive elements 
    of a ring and using this set the order.

Does anyone has arguments for (against) the first or the latter?

Christoph