Description: Define ordering relation on positive fractions. This is a "temporary"
set used in the construction of complex numbers df-c , and is intended
to be used only by the construction. Similar to Definition 5 of
Suppes p. 162. (Contributed by NM, 13-Feb-1996)(New usage is discouraged.)